>Given that there is no resources (or desire, as far as I can see) to >change the structure of Axiom
There is the desire. Axiom has a long term goal of introducing program-proof technology (either COQ or ACL2). ACL2 runs on the same lisp as Axiom. The plan is to load it into the Axiom image and make it support program proofs for spad code. I do not have the resources to attack this problem yet. I am still rewriting Axiom into literate form. However, I assure you that it is in Axiom's long-term goals, somewhere in the "30 year horizon". Look at http://axiom-developer.org (the Axiom home page) and see item (f), that's the program-proof goal. Tim Daly _______________________________________________ Axiom-mail mailing list [email protected] https://lists.nongnu.org/mailman/listinfo/axiom-mail
