[Axiom-developer] Axiom's Sane redesign musings

[Tim Daly]

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