Re: [Axiom-developer] sbcl and Axiom

[root]

> If we decorate the Categories with their mathematical axioms can
> > we prove anything about them? Can we do it automatically using ACL2?
> > Can we extend the compiler to do the proof while it compiles?
> 
> 
> Very difficult.

Clearly but I think that this is one of the most interesting areas
of research. Axiom has an advantage over other systems like Maple
and Mathematica because of our structure. In the long term it is
important that we are able to trust the results of computations,
especially when the results are beyond checking by hand. The only 
way to build trust will be proving the programs correct. Unlike
random programs, computer algebra programs have a good theory behind
them. I think it is vital that we develop a theory and a mechanism
for proof of computer algebra programs. It's the old Legendre vs
Gauss argument... we can't just assert that our programs are right,
we need to prove it. Otherwise it hardly qualifies as a science.

Also of interest is that computational math is not quite the same
as math. Axiom has some categories, such as RNG, which don't seem
to match those of regular math. One question is whether this is 
just a design flaw or does it expose a new computational object
that we need to examine theoretically.

The same issue arises in proofs. I often see statements that some
algorithm works "over the integers" and is of order O(n^2) or
some such. However, my computer does not have integers. It has
fixnums and bignums. The algorithm may be O(n^2) for fixnums but
become O(n^3) for bignum values. The standard methods of statements
based "on the integers" often don't take this into account.

Yeah, it's difficult but that's what makes it fun.

t