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" https://www.melconway.com/Home/pdf/committees.pdf [1] Conway's Law (youtube) https://youtu.be/5IUj1EZwpJY?t=1791 [2] Barbara Liskov CLU https://en.wikipedia.org/wiki/CLU_(programming_language)
