Conway's Law[0] basically says that software structure reflects organizational structure.
In the youtube video[1] the argument is made that, despite evolving organizational
changes, the old structure of software remains basically unchanged.
So it appears with Axiom. The Meta language was early work by Dick Jenks.
Portions of the effort still exist in Axiom despite removing the Meta compiler.
So Scratchpad's early organization still shines through.
Since the SANE effort is not a committee design but a single person effort things change.
Except for maintaining certain ideas like Liskov's CLU[2], Jenks/Trager/Davenport/et al.
ideas of group theory scaffolding, category-domain structuring, inheritance ideas, and
algorithms the Axiom SANE effort is a fundamental break from Axiom's past.
SANE is bringing the scaffolding idea to the forefront. It architects the proof technology
as a companion scaffold. LEAN-style definitions, axioms, and proofs are distributed
in parallel with the group theory category structure. The two are intimately connected
but separate. This preserves LEAN proofs yet enables the current code to reference
and inherit the proofs. It also provides a place for LEAN tactic algorithms.
Ultimately an Axiom domain inherits from both scaffolds so a function
not only inherits algorithms, it inherits definitions, axioms, and tacticsÂ
which can be used to prove a domain function is sound.
This break with the past undermines the effort, initially with Meta, then with
boot, to try to construct a surface language like spad. There are a lot of good ideas
for ensuring type safety in spad. However, it doesn't seem possible to add a proof
language by extending spad. Attempts at doing so result in a dead end.
Axiom's spad language is really just a domain-specific language on top of common lisp.
Apart from the inability to include proofs, two key problems are that spad code is not
well specified, making spad-level proofs questionable and that almost no-one speaks spad.
It makes more sense to revert to common lisp. This gives the full power of things like
CLOS and the macro facilities directly rather than "adding paint". A macro language
can mimic most of the features of spad without the struggle to build a compiler.
Axiom SANE keeps the algorithms and the structure but removes the paint.
Tim
[0] Melvin Conway "How Do Committees Invent"
[2] Barbara Liskov CLU