One long term Axiom goal is proving Axiom implementation of algorithms correct. After all, this is computational MATHEMATICS. The state of the art involves writing code but ignores the formal aspects. This is not acceptable for the long term. When Axiom gives an answer there needs to be some assurance that the answer is formally correct.
I'm climbing the learning curve for program proofs, trying to find a good way to handle something as complex as Axiom. There are three interlocking approaches, one for the algebra, one for the lisp code, and one for the machine level code. At the moment I'm spending most of my time at the lisp level. I've created a \sig macro so that the function signatures can be written out in haskell-like syntax. Gabriel Gonzalez gave an interesting talk, bridging the gap between programming and equational reasoning for program proofs. How to prove large software projects correct http://www.techcast.com/events/bigtechday8/maffei-1450/?q=maffei-1450 Using this approach requires some bottom-up construction of monoid behavior. I've marked "primitive" functions, that is, functions which are implemented using only common lisp function calls. These will be the early functions with signature maps. Once the signatures exist the code need to be refactored to have equational semantics. Once that is done each use has to be examined and refactored, recursively. This gives hope that we can create some equational proofs. This becomes more interesting when we look at lisp primitives used by the algebra. Refactoring the algebra's use of lisp into a single package would give Axiom-level semantics with proven code. Equational semantics for lisp-based algebra primitives will fit well in COQ, the tool that seems most likely to handle the algebra level. It looks like the pieces are slowly falling into place. SO much more to learn though... Tim _______________________________________________ Axiom-developer mailing list [email protected] https://lists.nongnu.org/mailman/listinfo/axiom-developer
