I've been living with Axiom's code now since the 1980s,
a portion of which I've authored or, at least, rewritten.
The code was written by some truly clever people (and
I'm not one of them). The parser, written by Bill Burge,
uses a "zipper" technique. It is quite clever and absolutely
opaque.
What has kept Axiom alive these 40+ years is that I
am one of the original authors, aware of the "how and
why", and able to answer (some) questions.
My experience and hesitation about SANE can best be
described by Peter Naur "Programming as Theory Building".
I strongly recommend reading the first 2.5 pages (up to 229).
The inability to transmit "tacit knowledge" will be the greatest
threat to the long term viability of SANE.
The path to a "proven Axiom" is becoming clearer. Unfortunately,
the breadth and depth of knowledge in both computer algebra
and proof theory needed to understand the result can take
many years. The learning curve is quite steep. Several professors
at CMU (Jeremy Avigad, Frank Pfenning, Robert Harper) have
made it possible for me to understand many leading-edge topics.
Maintaining the code will require a deep understanding
of CLOS, group theory, type theory, proof theory, etc. Even
with that background, the tacit knowledge embodied in the
design choices, like Burge's zipper parser, will still be opaque.
I've tried to capture some of it using Literate Programming
but it is clear there are things "you need to know" to understand
what is written and why it matters.
Creating an instance to show that "computational mathematics",
combining computer algebra and proofs, is possible is of
general interest. Creating a system that survives the effort is
rather unlikely. The conclusion is that SANE is not viable in
the long term.
Oh well, the joy is in the journey :-)
Tim