[Axiom-developer] Program Synthesis and Computer Algebra

[Tim Daly]

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)