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 hebi...@math.uni.wroc.pl _______________________________________________ Axiom-developer mailing list Axiom-developer@nongnu.org https://lists.nongnu.org/mailman/listinfo/axiom-developer