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

[Waldek Hebisch]

Tim Daly wrote:
> 
> 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?


That is pretty clear: there is algebra, there is interpreter
there is compiler.  For algebra one needs to specify what
each function is supposed to do and prove it.  There are
well-known notations for specifications and proofs, for
example Hoare triples.  Proof rules depend on language
used, but from point of view of proofs Spad is quite
conventianal imperative language, with a little syntatic
sugar for few constructs, so writing proof rules for
Spad is not hard.  Spad supports rich values (arrays, lists,
functions, types), so axiom for values will require
work.  Then one needs to prove compiler correct, for
this one needs specify meaning of output.  If the output
is Lisp, we need proof rules for Lisp, and we need to
prove that proof rules used for algebra are satisfied.
Finally we need some specification for interpreter
and we need to prove that interpreter satisfies this
specification.

The real question is how to do this.  Several years ago
my student did "by hand" a proof in Hoare logic of a simple 20
line long program.  The proof is 20 pages long.  The proof
is rather detailed, but he consided some facts as known
and some readers probably would ask questions demanding
more details.  While this is small sample it clearly
shows that doing proofs by hand is huge task and we
are unlikely to ever have needed resources.  Obvious
answer lies in automation.  But even with automation
this is still large task: the L4 operation system
kernel is clained to be proved correct with mechanically
verifed proof.  But that required about 8 lines of
proof annotations per line of executable code.
For me this is still too big to even start.  IMO
proving correctness will be reasible with better
proof assistants.  And there are signs that such
assistants may appear pretty soon (there was large
progress in last few years).

Let me repeat: it is not a question of what a proof is.
Already Turing around 1946 gave apropriate notion of proof.
The question is how.

BTW: Some people want proof to have be "certain" that
progam works.  Of course to get valid conclusion we
would have to prove lower layers.  I consider this
out of scope, but you may wish to prove that Lisp
implementation is correct in terms of machine
instructions and that logic of processor correctly
implements machine level.  We would also like to
have some assurance that gates do what they are
supposed to do.  Now, correctenss of gates is physics,
not math.  Correctness of processor is rather hard
to establish, because internal design is kept
secret.  But above what proof means is clear and
methods are known -- it is "only" problem of
huge effort needed for such work.


-- 
                              Waldek Hebisch
address@hidden