Axiom has a project goal of Proving Axiom Correct. This is computational mathematics. It needs a solid foundation.
There are limits to what can be proven, of course, but the power of the proof systems has really improved since Axiom was born. Of the half-dozen or more proof systems and it appears that COQ is closest to Spad in spirit. COQ has the ability to handle dependent types (e.g. specifying that an array has a fixed known length). COQ has the ability to generate OCAML programs from proofs. This will make it easy to compare with the Spad implementations. A major win in the long term would be to auto-generate the Spad code but that's a distant dream at the moment. Axiom is being attacked from two directions. The first is from the "categories down", trying to specify Axiom's category signatures in COQ. The second is from the "bits up", trying to specify the lisp functions that are implemented using only common lisp primitives. These are marked in the interpreter already and will soon have OCAML-like type signatures. If anyone knows of prior work on either path, please let me know. We have already gotten permission from Laurant Thery to use his work on the proof of Buchberger's algorithm, some of which will show up in Volume 13. I have to reverse-engineer his proof into the Spad implementation. Tim _______________________________________________ Axiom-developer mailing list Axiom-developer@nongnu.org https://lists.nongnu.org/mailman/listinfo/axiom-developer
