[Axiom-mail] Re: Axiom and program proof.

[root]

> Apologies for the delay in replying.

No problem. Rumor has it some people found employment after the
"crash of 2000" :-)

> 
> > My name is Tim Daly and I'm currently working on Axiom.
> > 
> > Axiom was withdrawn from the market on October of 2001. It was released
> > to me in September of 2002. I've been working along with others to make
> > it available as free software. It should be available in the near future.
> 
> Excellent! Do you have any plans to collaborate with the Aldor people:
> Aldor being the AXIOM extension language (www.aldor.org)? The leader of
> that project (Stephen Watt) was involved with AXIOM in the past.

Yes, I've had email conversations with Stephen and we're both
committed to maintaining compatibility. I've recently asked Stephen
to become an Aldor developer because I need Aldor running on the
Palm-pilot class of machines. I'm willing to do the work to port
it to that style of platform (more likely the Zaurus but something
in the handheld form factor).

> Hmmm, would I be right in thinking that you're the same Tim Daly whose was
> involved in AXIOM/Scratchpad and Aldor/A# originally? If so I guess that
> Stephen will need no introduction!

Yes, I'm the same Tim Daly, albeit a bit older and less wise. 
I wrote a tutorial for the Aldor compiler at one point in the
distant past.

> 
> I'd be interested to know when you release AXIOM as I'd love to be able to
> use it again.

You can find out the current status by visiting:
http://savannah.nongnu.org/projects/axiom

Particular plans and directions are available at the "homepage" link:
http://www.nongnu.org/axiom

The source code is not yet posted there. We are using a different
server for alpha development to ensure that the posted code at least
compiles correctly before we go public. Hopefully the interpreter and
algebra will arrive by year-end. It depends on how many vacation days
I get as this is a nights-and-weekend project.

> 
> > One of the threads of this development has been a discussion of proving
> > correctness of Axiom's algorithms. 
> > 
> > I have heard from Mike Dewar at NAG that you have worked in this area
> > in the past. I wonder if you have any continuing interest in the subject
> > or comments to share on this effort.
> 
> My PhD work was primarily aimed at assisting correctness analysis and
> proofs of Aldor programs rather than AXIOM programs per se although the
> same techniques could be applied. Also the emphasis was on generating
> verification conditions which could be checked or simply documented to
> enhance ones confidence in programs written using AXIOM/Aldor libraries
> rather than a full, formal verification of a particular program or
> routine.

I've downloaded and (lightly) read your thesis. The techniques are
interesting. In order to understand where I'm coming from I guess you
have to have a little background on the current direction of Axiom.

Axiom's being rewritten into a literate programming style using
a variant of Knuth's Web program built by Ramsey, called noweb. We plan
to define a standard format for these documents which we term "pamphlets".
I see from the thesis that you are already familiar with literate programs.

Pamphlets are intended to bring together the various parts of a particular
domain or topic including embedded code, design documents, examples, 
test cases, user documentation, proof, references to other pamphlets, etc.

The key problem with a system like Axiom is that it is nearly impossible
to fully understand the naked code without being aware of the background
theory. Unfortunately, the theory tends to be written in a Ph.D. thesis
which gets enshrined in a library and completely disconnected from, indeed,
often not even referenced by the source code.

I've gotten permission from various authors to include their Ph.D. work
into pamphlet files. I've embedded the source code into the thesis along
with more detailed explanations tying the thesis sections directly to
the code. The noweb program can extract the code for compilation or
construct the documentation with the embedded source code.

In this way I'm bringing together work by various authors who have
used Axiom. I want to ensure that the research work is available to
future users. 

One of the current efforts (see the homepage link above) involves
proving Axiom's algorithms correct. While I realize that this is a
huge task that will probably take years of work by many people I
believe that it needs to be done.

As computer algebra systems get larger it becomes impossible to be
an expert in the many domains they cover. However, as you point out
in your thesis it is important to know the assumptions made by these
systems. Relying on the fact that the code was written by experts in
their respective domains becomes insufficient as the system gets 
larger. 

Because Axiom is theory-based and strongly typed it is easier to 
verify and validate such a system (which, does not imply that it is
EASY to do so). However, unlike other programs that you might try
to prove (such as a text editor) Axiom is reasonably close to the
mathematics it tries to use. This gives us an advantage in two
directions. First, we have an underlying theory to guide the proofs.
Second, we don't need to descend to modelling the underlying system.
 
We're looking to attack problems of verifying and validating Axiom
at several levels. Your work (and Kelsey's work) provide a good
formalism that we can adopt as a standard for annotating the algebra
source code. To that end I'd like to be able to use your thesis (in
a modified form) to produce a noweb pamphlet that would be included
with Axiom. I'd expect that the thesis work would be spread over
two pamphlets, one annotating the SortPackage with an expansion of
your notation for those sorts and a second annotating defaults.spad
where our quicksort implementation lives.

I think that the work you've done can be useful to developers and
users of the existing system. Tom's work on Catdef.spad would make
excellent documentation of the catdef hierarchy.

> My personal view is that formally verifying the correctness of something
> the size of the AXIOM library is likely to be infeasible, particularly
> since the proof of some of the mathematics on which the algorithms are
> based may be very difficult (ie they are the result of published journal
> papers etc). I recall one of the authors/developers of the GAP computer
> algebra system mentioning that there is a function in GAP which is based
> on a "standard result" whose proof is given in a 57-page journal paper. I
> imagine that the same situation occurs in the AXIOM library.

We have been in discussions with the nuprl, now MetaPRL, developers to
examine the use of their methods to provide formal verification. They
have tackled large systems in the past (e.g. the French air traffic
control system) and appear to have the machinery to at least make a
significant dent in the problem. This will take a few years, of course,
but I'm looking toward a 30 year horizon for Axiom so I'm not concerned.

In fact, I believe that the intersection of Mathematics and Computer
Science forms the field of Computer Mathematics where you'll be expected
to not only prove your theoretical result but also to reduce it to
practice in a proven form. That this area will someday be a recognized
department within Universities is inevitable.

> However, one can probably have confidence in many of the AXIOM functions
> from the fact that the authors of the functions are probably the same
> people who wrote papers on the same subject (either the maths behind them
> and/or the algorithms themselves). Indeed some of the papers may use AXIOM
> or Scratchpad code as specific examples of the results of their research.

I've already rewritten portions of a thesis into a pamphlet for the
domain of Denavitt-Hartenburg Matrices (dhmatrix.spad). I've had
discussions with Dr. Sit for doing the same with his research work in
partial differential equations (pleqn.spad).

I'm not particularly worried that the implementations are wrong. The key
concern is that the mathematics continues to move. In order to keep a
system like Axiom alive we need to make it possible to understand the
existing code so it can be modified by the next generation of Ph.D.
students.

> My work was involved with the use of pre- and post-conditions on Aldor and
> AXIOM functions: the main aim was that we trust that the algorithms behave
> as specified in their pre/post conditions but that the algorithms may be 
> used in inappropriate ways or settings by users/developers. In my work the 
> user would take their code and propagate the pre/post conditions from the 
> AXIOM functions into it. Any time an AXIOM function is used they/we would 
> generate a verification condition that the pre-condition holds. Assuming 
> that it does we can extend the database of knowledge about the program 
> with the post-condition of the function.
> 
> For correctness proofs you would take the opposite direction: given the
> pre- and post-conditions of a function, can you show that the code behaves
> correctly wrt it specification?
> 
> A major issue here that I've skirted over is "where do the specifications
> come from?": some may be present in AXIOM documentation but to perform a 
> formal verification you would need a formal specification of how a given 
> function is intended to behave before you can even begin to check whether 
> or not it does behave correctly wrt that specific. That could be a mammoth 
> task in itself.
> 
> If you're interested you can get my thesis here:
> 
>    www-theory.dcs.st-and.ac.uk/~mnd
> 
> (or at least it can once the server and network links are working). I can 
> email you a copy in PostScript form if you wish.

Actually, I'd prefer a TeX form of the document provided you were willing
to let me rework it into a pamphlet form.

> The strong typing of AXIOM and Aldor means that interesting pre- and
> post-conditions are mostly handled by the type system so a lightweight 
> verification system that I described in my thesis isn't really needed for 
> validating AXIOM functions.
> 
> For example, in C one might specify an integer sqrt function:
> 
>    int isqrt(int x);
>       // requires x >= 0
>       // ensures  (result*result <= x) /\ (x < (result+1)*(result+1))
> 
> Then if someone writes a program containing:
> 
>    /* ... */
>    a = isqrt(b);
> 
> we can generate a verification condition that "a >= 0" and add to our 
> database of knowledge that after this line we know that:
> 
>    (a*a <= b) /\ (b < (a+1)*(a+1))
> 
> However, in AXIOM you would probably define isqrt over PositiveInteger and
> so the pre-condition isn't needed anymore.

This is where I see Kelsey's thesis work being applied. He has done
work on catdef.spad which is the basis of the Category towers.

> Also in AXIOM the domains of computation are often closed (groups, rings, 
> fields etc) so you're unlikely to have strange functions like isqrt: your 
> algorithms will generally accept all inputs provided that they satisfy the 
> type constraints on the function arguments. The type of the return value 
> of the function would probably be chosen according to the range of the 
> function being implemented to avoid the need for post-conditions.
> 
> [It's a few years since I worked in this area so my terminology may be 
> rather weak - my apologies].
> 
> Hope this goes some way to answering your question. I'm afraid I don't
> have much of a continuing interest in this field as I'm now heavily
> involved with another completely unrelated project at another university
> (planet surface simulation for testomg vision-based landers).

Kewl. I did masters work in machine vision and ended up doing industrial
robotics centuries ago. It's really a fun area. Of course you're working
with cameras that are slightly higher resolution than 32x32 pixels.

> I am, in theory at least, still assisting with maintenance and development
> of the Aldor compiler but I've been too busy to do any work on that for a
> year now. I am interested in being able to use AXIOM again though!

This is the problem with free software. You have to make it possible for
the next generation (which could mean NEXT YEAR) to pick it up and carry
it forward.

Tim