Hill Climbing.... Almost every possible step along the path to creating the SANE version of Axiom involves a LOT of hill climbing, by that I mean a LOT to learn to get started.
Axiom was built with a scaffold of group theory which makes it easier to reason about and understand. Going forward we need to use the theories we have learned since the 1980s to ground the system properly. One hill is that there is almost no documentation or even literature reference for many of Axiom's algorithms. Some were done as PhD research; many were ad-hoc "it works for me", etc. Axiom already has decorated some of the algorithms with literature references. More needs to be done. As for hills, there is the large area of logic which has many different branches. One has to crawl from one corner of the lambda cube to the other in order to know what dependent types are and how to use them. https://www.cs.uoregon.edu/research/summerschool/summer12/curriculum.html Then there is the category theory area since we would like to have things like definitionally correct functors. https://www.youtube.com/watch?v=Y5YCE_mVjvg&list=PLhgq-BqyZ7i7MTGhUROZy3BOICnVixETS Then there is the whole area of proof. Currently Axiom is focusing on Lean as the underlying machinery as it seems to be the leading edge in constructive type theory and mathematics. https://leanprover.github.io There are many different approaches to specification ranging from "hand waving" (UML) to strong theory. But transitioning from the specification to the code is still a huge gap. https://formal.iti.kit.edu/~beckert/teaching/Spezifikation-SS04/11Z.pdf Programming has also advanced. Clojure has raised some significant issues of concurrent and scalable programming. It would be great if matrix algorithms could be run in parallel. https://clojure.org/about/concurrent_programming Symbolic-Numeric programming has been an issue. There is every reason for numeric programs to have a "place at the table" in a computational mathematics system. There are interesting issues that arise. https://www.amazon.com/End-Error-Computing-Chapman-Computational/dp/1482239868 Of course, none of this gets anywhere near the issues of proving programs correct, that being the central question. Then there is the question of creating a compiler that uses and integrates all of the above as well as being able to handle the current Axiom algorithms. But the compiler needs to also recognize and propagate the logical definitions and axioms along the inheritance paths. Of course, the compiler and interpreter should have the same semantics and work on the same data structures so that what compiles will interpret and what interprets compiles. That doesn't even mention the supposedly trivial issue of replacing the front end, hyperdoc, and graphics with a portable browser interface. CSS seems to be a whole career skill at this point. Plus it really should work well in the whole "workbook" environment like CoCalc. Progress is being made in all of these areas but, as you can imagine, it takes a lot of thought to combine them cleanly. Tim