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