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
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
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
Waldek,
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
I have some experience with ACL2, ACL2 uses a very small subset
of common lisp, there are no side effects and no higher order
functions, although Axiom is written in a pretty small subset of CL, it
will be very difficult or require unimaginable mount of work to prove
the Spad compiler is correct
Thanks. I had not heard of PVS but I will look into it.
I have used ACL2 in the distant past and will have to get up
to speed on it again. I've downloaded and built the latest version.
I know that ACL2 is not capable of handling a Spad compiler but one
has to start somewhere. The important
This was Master Thesis, unpublished and in Polish. This
is work that students are supposed to do to get finish
their study and get Master degree. Most of the work
presents material from literature, the proof is original.
I can send you a .ps file if you want.
My command of English is marginal
The society of scientists, the community of scientists, has
this advantage, that from the moment we enter it, we all know
that fifty years from now, most of the things we learned here
will turn out not to have been quite right.
-- Jacob Bronowski, Silliman lectures, Yale 1967
