Sane: "rational, coherent, judicious, sound" Axiom is computational mathematics, of course. The effort to Prove Axiom Sane involves merging computer algebra and proof technology so Axiom's algorithms have associated proofs.
The union of these two fields has made it obvious how far behind Axiom has fallen. Mathematicians and some computer languages (e.g. Haskell) have started to converge on some unifying ideas. As a result, the new Sane compiler and interpreter needs to consider the current environment that mathematicians expect. This falls into several areas. 1) SYNTAX It is clear that Axiom's syntax and user interface has not kept up with the proof technology. A trivial example is a signature. Axiom likes: foo : (a,b) -> c whereas Lean / Coq / or even Haskell prefers foo: a -> b -> c Given that many systems (e.g. Haskell) use the second syntax we need to consider adopting this more widely accepted syntax. 2) PROOF and SPECIFICATIONS And, obviously, Axiom does not support 'axiom', 'lemma', 'corollary', nor any specification language, or any language for proof support (e.g. 'invariant'). Mathematicians have these tools readily available in many systems today. 3) USER INTERFACE Axiom's command line interface and hyperdoc were fine for its time but Lean and Coq use a browser. For example, in Lean: https://leanprover.github.io/tutorial/ or in Coq: https://jscoq.github.io/ The combination of a browser, interactive development, and "immediate documentation" merges a lot of Axiom's goals. 4) CATEGORY STRUCTURE William Farmer and Jacques Carette (McMaster University) have the notion of "tiny theories". The basic idea (in Axiom speak) is that each Category should only introduce a single signature or a single axiom (e.g. commutativity). It seems possible to restructure the Category hierarchy to use this model wilthout changing the end result. 5) BIFORM THEORIES Farmer and Carette also have the notion of a 'biform theory' which is a combination of code and proof. This is obviously the same idea behind the Sane effort. 6) INTERACTIVITY As mentioned in (3) above, the user interface needs to support much more interactive program development. Error messages ought to point at the suspected code. This involves rewriting the compiler and interpreter to better interface with these tools. Axiom already talks to a browser front end (Volume 11) interactively but the newer combination of documentation and interaction needs to be supported. Sage provides interactivity for some things but does not (as far as I know) support the Lean-style browser interface. 7) ALGORITHMS Axiom's key strength and its key contribution is its collection of algorithms. The proof systems strive for proofs but can't do simple computations fast. The proof systems also cannot trust "Oracle" systems, since they remain unproven. When Axiom's algorithms are proven, they provide the Oracle. 8) THE Sane EFFORT Some of the changes above are cosmetic (e.g. syntax), some are "additive" (e.g. lemma, corollary), some are just a restructure (e.g. "tiny theory" categories). Some of the changes are 'just programming', such as using the browser to merge the command line and hyperdoc. This involves changing the interpreter and compiler to deliver better and more focused feedback All of that is "just a matter of programming". The fundamental changes like merging a specification language and underlying proof machinery are a real challenge. "Layering Axiom" onto a trusted core is a real challenge but (glacial) progress is being made. The proof systems are getting better. They lack long-term stability (so far) and they lack Axiom's programming ability (so far). But merging computer algebra and proof systems seems to me to be possible with a focused effort. Due to its design and structure, Axiom seems the perfect platform for this merger. Work on each of these areas is "in process" (albeit slowly). The new Sane compiler is "on the path" to support all of these goals. 9) THE "30 Year Horizion" Axiom either converges with the future directions by becoming a proven and trusted mathematical tool ... or it dies. Axiom dies? ... As they say in the Navy "not on my watch". Tim _______________________________________________ Axiom-developer mailing list Axiom-developer@nongnu.org https://lists.nongnu.org/mailman/listinfo/axiom-developer