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". https://pages.cs.wisc.edu/~remzi/Naur.pdf 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