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

[Martin Baker]

Tim,

Yes, I think it would be really good if Axiom could live up to its name 
and include axioms.

It seems to me that categories in Axiom are mostly about function 
signatures (I know I'm vastly oversimplifying here) but they would be 
more like the mathematical concepts they represent if they included axioms?

Are you talking about two different types of capability here:
* Proof Assistants like 'Coq' or 'Isabelle'.
* Algebraic Specification Languages like 'CASL'.
Does ACL2 fit into this distinction?

So I'm thinking that proof assistance are based on rules and driven by 
human input and algebraic Specification Languages are based on axioms 
and provide some level of automatic checking, although I guess there is 
some overlap?

I get the impression that Axiomatic systems are problematic in that a 
single error allows you to prove anything (true=false) and, as you have 
pointed out to me, rule based systems are difficult to debug.

Even so, I think that the addition of axioms into categories would be a 
big benefit, even it it was only initially used for human readers and 
some automated checking.

The choice of what rules to call axioms may be arbitrary but there are 
all sorts of choices that have to be made when supporting an algebra, 
like notation and which algorithm to use, which don't follow 
automatically from the mathematics.

> What would it mean to prove Axiom correct?

I get the impression that, at some level a computer program is only an 
approximation to mathematics (float approximates to reals and so on). 
Issues with proving code(algorithms) - 'halting problem'. Despite these 
limits to a complete proof of the whole program, there is a lot that can 
be done at a higher level if axioms were included in the program.

So I think this sort of capability would be really good, I'm just too 
impatient to wait 30 years.

Martin