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
_______________________________________________
Axiom-developer mailing list
[email protected]
https://lists.nongnu.org/mailman/listinfo/axiom-developer
