Re: [Axiom-developer] Why proving Axiom correct is important

[daly]

Martin,

>The book is based around Isabelle/HOL so if you don't want to use 
>Isabelle the book may not be of interest to you? I have only just 
>started reading the book so I don't have any great insights to give.

Actually, Lamport's "How to write 21st Century Proofs" and 
"Specifying Systems" is the most recent bit of study. He has talks
on Youtube about it.



>I get the impression that what proof assistants / interactive theorem 
>provers are about is proving equations/theories from other theories 
>using logic and proof methods like induction. I think what you are 
>talking about is proving algorithms correct (Semantics?) this is covered 
>in part 2 of the book. Do you think these sort of approaches: 
>Denotational Semantics, Small-step Semantics, Big-step Semantics and so 
>on are what you are aiming at?

We really need "full stack" proofs. COQ/TLA for the Spad to Lisp layer
(since Spad is really just a domain-specific language on a lisp base).
ACL2 for the Lisp to C layer (since we use GCL), LLVM to ACL2
translator for the C layer (the Vellvm effort), and CCAs (Conditional
Concurrent Assignments, for Intel machine instruction semantics, my
prior research work) for the C to machine layer.




>I get the impression that using a separate proof assistant is not ideal 
>and there would be a lot of advantages in combining the symbolic algebra 
>program (Axiom) with the logic/proof assistant. Apart from anything else 
>the learning curve is as steep as Axiom! The problem for me is the 
>massive and confusing overlap of these types of program. Not just the 
>program but, more importantly, the libraries. As you can see from the 
>libraries here:
>http://isabelle.in.tum.de/dist/library/HOL/index.html
>it contains most of the same algebras as Axiom but in a slightly 
>different hierarchy.

ACL2 is in Common Lisp and can be layered underneath Axiom so that
some of its capabilities can be exposed as domains/packages. This
would allow proofs to be expressed in Spad as a mathematical feature.
It would also allow automatic checks during builds. This existed 
locally but was never pushed into the repository.

One should be able to do ")exhibit gcd" to see the proof support
for the function and ")exhibit GCDDOM" to see the category proof.
These ought to be static objects once the proof exists.



>A possible first step would be to encode axioms/rules/identities in each 
>Axiom category/domain. If nothing else this would allow automatic 
>generation of test code at random values, this is not proof but it would 
>be a first step to proofs at a later stage.

There exists a few mathematical axiom statements in the category book
(Volume 10.2), associated with each category (look at SemiGroup for
example). The intention is to decorate all of the categories and
domains with mathematical axioms which can be assumed in the proof.

Much more work needs to be done to just look up the standard axioms
for the various categories. Feel free to contribute by looking up
what the group/ring/field/etc axioms should be. They will be added
to the approprate categories.

The plan is to add an "axioms" category with an "axioms" function
export so you can query the axioms that something should obey from
code or the command line.




At the lisp level (Volume 5 Interpreter, Volume 9 Compiler), there is
a new Latex tag \sig which supports Haskell-style signatures for lisp
code. (See intloopPrefix? for an example.) The intention is to add
signatures to all of the functions. This will allow the proof engine
to move along the signature space.

Along with this effort the interpreter/compiler is being slowly
redesigned to be more functional-programming oriented. The plan is to
remove the globals, create lisp-level types using defstructs, and
introduce strict type decorations using lisp declare statements.
Removing/hoisting side-effects is an essential step. 

There is a book called "The Semantics of Destructive Lisp" (free pdf
online) which talks about functions which modify their arguments and
internals, as Spad is known to do. There is also work on the
Denotational Semantics of Lisp. Fred Blair wrote a paper defining
the denotational semantics of Lisp/370 years ago.




The proof volume (Volume 13) is taking a middle-out approach, starting
with an attempt to prove Axiom's implementation of Euclid's algorithm.
The goal is to "work at the coal-face" of the problem to see what is
needed and what works. Pointers to online versions of Euclid proofs
are most welcome.

Tim