Conway's Law, Axiom, and Axiom SANE

--000000000000d2eada060346d897
Content-Type: text/plain; charset="UTF-8"

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)

--000000000000d2eada060346d897
Content-Type: text/html; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable

<div dir=3D"ltr"><div>Conway&#39;s Law[0] basically says that software stru=
cture reflects organizational structure.</div><div><br></div><div>In the yo=
utube video[1] the argument is made that, despite evolving organizational</=
div><div>changes, the old structure of software remains basically unchanged=
.</div><div><br></div><div>So it appears with Axiom. The Meta language was =
early work by Dick Jenks.</div><div>Portions of the effort still exist in A=
xiom despite removing the Meta compiler.</div><div>So Scratchpad&#39;s earl=
y organization still shines through. <br></div><div><br></div><div>Since th=
e SANE effort is not a committee design but a single person effort things c=
hange.<br></div><div>Except for maintaining certain ideas like Liskov&#39;s=
 CLU[2], Jenks/Trager/Davenport/et al.</div><div>ideas of group theory scaf=
folding, category-domain structuring, inheritance ideas, and</div><div>algo=
rithms the Axiom SANE effort is a fundamental break from Axiom&#39;s past.<=
/div><div><br></div><div>SANE is bringing the scaffolding idea to the foref=
ront. It architects the proof technology</div><div>as a companion scaffold.=
 LEAN-style definitions, axioms, and proofs are distributed</div><div>in pa=
rallel with the group theory category structure. The two are intimately con=
nected</div><div>but separate. This preserves LEAN proofs yet enables the c=
urrent code to reference</div><div>and inherit the proofs. It also provides=
 a place for LEAN tactic algorithms.<br></div><div><br></div><div>Ultimatel=
y an Axiom domain inherits from both scaffolds so a function</div><div>not =
only inherits algorithms, it inherits definitions, axioms, and tactics=C2=
=A0</div><div>which can be used to prove a domain function is sound.</div><=
div><br></div><div>This break with the past undermines the effort, initiall=
y with Meta, then with</div><div>boot, to try to construct a surface langua=
ge like spad. There are a lot of good ideas</div><div>for ensuring type saf=
ety in spad. However, it doesn&#39;t seem possible to add a proof</div><div=
>language by extending spad. Attempts at doing so result in a dead end.</di=
v><div><br></div><div>Axiom&#39;s spad language is really just a domain-spe=
cific language on top of common lisp.</div><div>Apart from the inability to=
 include proofs, two key problems are that spad code is not</div><div>well =
specified, making spad-level proofs questionable and that almost no-one spe=
aks spad.</div><div><br></div><div>It makes more sense to revert to common =
lisp. This gives the full power of things like</div><div>CLOS and the macro=
 facilities directly rather than &quot;adding paint&quot;. A macro language=
 <br></div><div>can mimic most of the features of spad without the struggle=
 to build a compiler.<br></div><div><br></div><div>Axiom SANE keeps the alg=
orithms and the structure but removes the paint. <br></div><div><br></div><=
div>Tim<br></div><div><br></div><div>[0] Melvin Conway &quot;How Do Committ=
ees Invent&quot;</div><div><a href=3D"https://www.melconway.com/Home/pdf/co=
mmittees.pdf">https://www.melconway.com/Home/pdf/committees.pdf</a></div><d=
iv><br></div><div>[1] Conway&#39;s Law (youtube) <a href=3D"https://youtu.b=
e/5IUj1EZwpJY?t=3D1791">https://youtu.be/5IUj1EZwpJY?t=3D1791</a></div><div=
><br></div><div>[2] Barbara Liskov CLU</div><div><a href=3D"https://en.wiki=
pedia.org/wiki/CLU_(programming_language)">https://en.wikipedia.org/wiki/CL=
U_(programming_language)</a></div><div><br></div></div>

--000000000000d2eada060346d897--