[Axiom-developer] Computational Mathematics, proofs, and correctness

[daly]

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