Re: [Axiom-developer] Call for help

[daly]

>You will have to excuse me if I dozed off in the back seat during the
>trip.  Is this where we are?

We're still lost but things have changed a bit since the 80s.

>We have a programming language (say SPAD or lisp) and a program in
>that language represented by a series of statements.

>The intent is to construct, in a literate manner, a series of
>statements in MPL and SPAD that are flagged and readable by the
>respective compilers such that if the MPL statements are logically
>correct (assertions match conclusions) then SPAD will also reach the
>same conclusions as you stated in MPL.  Presumably that is also done
>by MPL via a dictionary or some such.

>For instance in Left Module Construction the assertions are equivalent 
>to a triple F: (R(\cdot , +),G(+),RxG->G(+) and the base qualification is:
>R is a ring
>G is a group
>RxG is legitimate map from R,G to G
>etc...
>And fail (hopefully informatively) if one of these fails
>or Return a construct that has all of the functional properties of Left 
>Modules.

>Now the literate program has a "model" of Left Module in MPL and then
>checks the SPAD code to see if it correctly does all the of the above
>checks.  If you have done all that then it seems to me that there
>should also be a "hook" that check my custom code as well; of course
>that should be optional and only done when required.  And requires
>that I can define my expectations for my code (which unfortunately I
>sometimes can't).

>Forgive any ignorance but I left off back in the 80's with a Sandia (I
>think) formalism to check the correctness of code.  That is: make
>assertions about what the code will do with the input and verify that
>the code does that.  To give credit this was supposed to be done by
>first order predicate expressions that can be verified.

>I would appreciate constructive corrections and suggestions.

It depends on what horizon we're discussing. There are at least 3
"in plan" at the moment, although like everything that isn't in
running code, this is subject to change.

THE NEAR TERM HORIZON

The near-term goal is to get the "first turn of the crank".
This first step in happening now. 

Lisp Level Code

At the lisp level I've begun marking the code with two pieces of
information, a haskell-like type signature and a "level" indicator.
Lisp-level data structures will initially be used. These will get
closer to the Spad-level types (e.g. constructors) as the code gets
closer to Spad, which from the lisp viewpoint nothing more than a
domain-specific language (DSL).

The "level" indicator marks code with its "height" in the lisp
hierarchy. Code which is pure common lisp is marked at level 0.
Code implemented using only common lisp and level 0 code is level 1,
etc. This allows us to crawl up the code from ground-level.

Lisp-level code is being proven using ACL2 and side-level proofs.
That is, the "proof" is a version of the code that fits within the
ACL2 constraints (e.g. is not using floats). Some ACL2 code is
directly executable Common Lisp and will be used verbatim.

Currently this proven code is automatically extracted at build time
and given to ACL2 to prove.

Spad Level Code

At the Spad level, it appears that COQ is the closest in spirit.
COQ allows dependent types (e.g. arrays with fixed length) and
executable primitives so properties can be defined by code.

Here the game is to decorate the categories with mathematical
axioms. These axioms will be (re-)stated in COQ so they can be 
used in proofs. The axioms are spread across the categories and
inherited using the same hierarchy as the category structure.
Thus Group inherits from Ring, etc.

Some categories provide default code. This will be the first
level of attack using COQ, trying to prove that the code conforms
to and correctly implements the axioms.

Machinery needs to be created to put these axioms into the
system in an effective way. For instance, )show should be able
to aggregate and display the inherited collection. The proof
extraction machine needs to be able to collect and assert the
axioms prior to proof.

Currently this proven code is automatically extracted at build time
and given to COQ to prove. COQ contains support for things like
integer arithmetic so this will help with the circular reference
issue.

"Other level" code

Axiom compiles to C using GCL. There is work based on LLVM that
supplies proof technology. C compiles to i86 machine code. I have
written a program which takes i86 binary code and produces 
conditional-concurrent assignments (CCA) which define the machine
level semantics of each Intel instruction. The CCAs can be
combined to produce the semantics of blocks of code. 
(see http://daly.axiom-developer.org/intel.pdf)

So there are the beginnings of "full stack" proof technologies
from Spad to machine code. In the near term we only care about
the Spad and Lisp code.

Expectations

This will be a learning experience. It is expected that the effort
will uncover bugs, misconceptions, and unprovable hypothesis cases.

THE MIDDLE TERM HORIZON

The near term proofs are "side-proofs" that sit alongside existing
code. However, we have complete control over the Spad-to-Lisp compiler
so it is possible to generate the proof code from the Spad code. We
also have complete control over the Lisp-to-C compiler so it is
possible to generate the proof code from the Lisp code. Even now some
ACL2 Lisp code is directly executable and I expect this trend to
continue.

This will certainly cause existing code to be reshaped, rewritten, and
reorganized. It will also make code even harder to write. But the
benefit is much higher confidence in the answers provided.

Since this will take a long time we can hope that the tools we use
will be much better. Quite a few things have changed since I used
NTHQM back in the distant past. I expect they will continue to change
for the better.

THE LONG TERM HORIZON

Computational mathematics is more constrained than general mathematics.
Proofs need to be constructive and need to account for more details. 
That said, it is still mathematics. We can and should demand that 
Axiom is "correct" for some provable version of "correct".

Already there are proofs of some algorithms. I have a proof of
Buchberger's algorithm. Ideally this proven code and its associated
proof can be directly inserted into Axiom.


This is a lot of work. Fortunately Axiom has a 30 year horizon so
there is plenty of time.

Tim