One interesting side-discussion of proving Axiom sane is that there

is a connection to the area of program synthesis.

At the moment, the program synthesis field is in a very early stage.

See, for instance [0] which generates algebra problems from specs

by using "similarity".

In the proof area of computational mathematics, some systems are

able to generate programs from the proof.

So in the computer algebra branch of computational mathematics

it is likely that interesting algorithms can be generated.

In particular, once it is possible to generate specifications from

Axiom's Category and Domain decorations, it should be possible

to construct specifications and then generate programs from these

specifications that are "Axiom compatible".

This will likely be a future research path as a direct spinoff of the

Axiom proof effort.

Tim

[0] Singh, Rohit, Gulwani, Sumit, and Rajamani, Sriram

"Automatically Generating Algebra Problems" AAAI'12 (2012)

_______________________________________________

Axiom-developer mailing list

[hidden email]
https://lists.nongnu.org/mailman/listinfo/axiom-developer