I've been working on proving Axiom correct for years now.
I've spent the last 18 months learning proof systems and
deep-diving into the theory (thanks, in part, to Carnegie
Mellon's Computer Science Department giving me the
"Visiting Scholar" appointment and faculty access).
I've "discovered" that there are two large, independent,
and largely parallel efforts in computational mathematics.
There is the computer algebra field, where we spend most
of our time and effort. The concentration is on finding new
algorithms. This is interesting and quite satisfying. It appears
to be "progress". There is a large body of literature.
There is the program proof field, where a large number of
people spend most of their time and effort. The concentration
is on building systems to prove programs correct. On some
occasions a computer algebra algorithm, like Groebner basis,
is proven. There is a large body of literature.
Surprisingly though, there is little overlap. It is very rare to
find a paper that cites both Jenks (CA) and Nipkow (PP).
In fact, without a great deal of background, the papers in the
program proof field are unreadable, consisting mostly of
"judgements" written in greek letters. Or, coming from the
proof field, finding the computer algebra "algorithms" lacking
anything that resembles rigor, not to mention explanations.
Both fields are very large, very well developed, and have been
growing since the latter half of the last century.
It is important to bridge the gap between these two field.
It is unlikely that anyone will invest the millions of dollars and
thousands of hours necessary to "rebuild" an Axiom-sized
computer algebra system starting with a proof system. It is
also unlikely that anyone will succeed in proving most of
the existing computer algebra systems because of their
ad hoc, "well-it-mostly-works", method of development.
Axiom has the unique characteristic of being reasonably well
structured mathematically. It has many of the characteristics
found in proof-system idea like typeclasses (aka Axiom's
"Category-and-Domain" structures. What Axiom lacks is the
propositions from typeclass-like systems.
So the path forward to unite these fields is to develop the
propositional structure of Axiom and used these propositions
to prove the existing algorithms. Uniting these fields will bring
a large body of theory to computer algebra and a large body
of algorithms to a grounded body of logic.
Tim