One of Axiom's project goals involves proofs of the computational mathematics.
In plan, but not yet attacked, is the question of proving Axiom. Axiom claims to be "computational mathematics", after all. This raises a lot of thought bubbles, but most interesting to me at the moment is what the goal means. There seems to be several interpretations and my shower committee (i.e. what I mutter to myself about in the shower) seems unfocused. The top level question is: What would it mean to prove Axiom correct? The first interpretation is computational. The second interpretation is mathematical. The third interpretation is both computational and mathematical. Consider these in order. From a computational point of view Axiom is a big lisp program. It implements a domain specific language called Spad which compiles to lisp programs. ACL2 [0] is ideal for proving programs at this level. ACL2 is also a lisp program and could easily be co-resident with Axiom in a lisp image. Models can be defined and proved to have certain properties. The lisp code could be decorated with theorems and lemmas. This would make it possible to bring much more rigor to the implementation. It provides an opportunity to define a model for interpreting and compiling Spad which can be used to check the implementation. >From a mathematical point of view, Axiom is an implementation of abstract-algebra-like categories and domains. One could consider decorating the Spad algebra code with axioms (e.g. the abelian group axioms) and theorems. COQ [1] seems ideal for proving Spad code at some level of abstraction. Of course, Spad's view of algebra differs somewhat from the abstract algebra scaffold. Proving an algorithm (e.g. finding primes) over all possible domains is really a non-trivial task. >From a computational and mathematical point of view, there is what I call the "kittens" problem, as in, "it is kittens all the way down" (cause, yaknow, the internet doesn't like turtles). What does it mean to prove something in Axiom? Is doesn't seem sufficient to prove that the interpreter/compiler provide a correct translation of Spad. Nor does it seem sufficient to prove that a Spad domain properly preserves the commutative property. What I'd like to achieve (and, given that we are just starting toward a 30 year horizon we have plenty of time), is some confidence that Axiom programs can be used with some reasonable degree of assurance that it does what it says on the tin. At the moment, computational mathematics seems to "float" on nothing. I am deeply unhappy with the current state of the art. The current state makes it hard for a computer scientist to see where the interpreter/compiler needs work. The current state makes it hard for a mathematician to see where integration needs work. That we are decades into the collision of mathematics and computers yet have no standards of proof is, to my mind, unacceptable. The computer scientist side of me wants some form of non-computational model of the interpreter/compiler. The mathematician side of me wants some convergence of the algebra and mathematics. We can do better. In fact, any attempt at all would be better. Even if nothing were formally proved I'm sure the side-effect would be a better, more trustworthy Axiom, which is a worthwhile goal. Nobody wants their "Ph.D recalled" due to a bug in Axiom. :-) Excelsior! Tim Daly [0] Kaufmann, Matt; Moore, J Strother ACL2 Version 6.4 http://www.cs.utexas.edu/~moore/acl2 [1] various The Coq Proof Assistant http://coq.inria.fr _______________________________________________ Axiom-developer mailing list Axiom-developer@nongnu.org https://lists.nongnu.org/mailman/listinfo/axiom-developer