[Axiom-developer] How to prove large software projects correct

[daly]

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