ACL2
>Just to throw into the mix given the thoughts you express below, acl2
>builds within the same gcl image as axiom, and might be useful for your
>theorem proving needs.
ACL2 is useful for hardware verification. It might be useful for validating
the FPGA configuration. However, the Verilog language eventually
generates a binary image to be loaded. I'm unaware of any effort to
connect ACL2 to the Verilog toolchain. I'll look again just to be sure.
ISOLATION
>I do understand that you have determined it better to work in a more
>isolated fashion -- makes sense. Do you intend your work to be made
>available to end users in precompiled and/or source form from time to
>time? This question AFAICT is entirely apart from whether or not you
>want to avoid team management in a typical 'foss' setting. I am sorry
>that your experience with 'open source' was found to be counter
>productive.
I'm working "in a more isolated fashion" but not particularly by a
deliberate choice. Everyone simply left the project.
I think this is due to a matter of philosophy. Axiom is an amazing
effort, carefully built using the leading theories of the time, such as
work by Barbara Liskov on CLU[0]. I think it is important to preserve
it, hence my efforts. Apparently no-one agrees. Waldek does amazing
work. Who will follow after him?
PRESERVATION
The "literate programming goal" is a preservation task.
Axiom is complex. To develop within it requires a great deal of effort.
To maintain it requires even more effort. The long term problem is
the lack of explanation (not documentation). Who is going to maintain
the compiler / interpreter? What are daase files? What theories
underlie the algorithms? What are the literature references and
PhD thesis references?
The "computer algebra test suite goal" (CATS [1]) is a preservation task.
It is an effort to test Axiom versus various existing bodies. You can see the
Kamke suite, Albert Rich's suite, etc. The goal was to develop a comprehensive
suite testing all of Axiom, such as the untested Clifford Algebra work.
The "merge with existing systems goal" is a preservation task.
Merging had two streams. The first was libraries. I have re-created BLAS
and LAPACK in Lisp so they can be called directly. I also pushed to
connect Axiom to William Stein's SageMath work, done by Bill Page just
before the fork festival.
Preservation goals are fine. I did a lot of literate work and test work.
RESEARCH
My real interest is further research.
The "prove Axiom correct goal" is what I'm still pursuing. This is a
much deeper, non-preserving "research" goal. It is time for the two
streams to merge. The 6 years I spent as a "visiting scholar" at CMU
was used to understand the proof work. A side effect, since I was in
the computer science department, was a much deeper understanding
of dependent type theory and category theory.
Axiom, unlike other systems, is built on a group theory scaffold.
This give it a near-perfect architecture to include theorems and proofs.
The inheritance mechanism needs to be extended to inherit these
theorems, collecting them up at the point a function is defined so
they can all be used to prove the function correct. Here "correct"
is with respect to the function specification, which leads to another
path of a specification language.
There are difficult practical problems and difficult research problems.
Practically, for example, the proof theory crowd has no focus on
organizing theorems so they match Axiom's category structure.
Finding, reshaping, and possibly re-proving theorems to fit Axiom
is one of my more tedious paths to tread. I should note that the
proof crowd strongly rejects the notion of proving programs correct.
The resistance to merging is not only on the computer algebra side.
Research problems are everywhere, even seemingly mundane
things like re-proving the Groebner basis algorithm in an Axiom
hierarchy. Much deeper problems include the limits of fully
dependent types (which, in theory, include all of lisp and Axiom
to instantiate a type). Or ensuring that the system fully supports
functors from category theory. Or the issue of termination[2], etc.
I see Axiom as a research platform. In an ideal world it has more
than enough problems to spin off PhD students for years to come.
SIMPLIFY, SIMPLIFY
>If so, as you work, hopefully in a public area like github, and
>determine at some point that a snapshot should be taken, I can help make
>sure the result doesn't suffer from bit rot by keeping the build
>machinery current within Debian and equivalents.
Let's look at history. I killed the Meta compiler and Dick Jenks lost
his mind over it (it was his research product). I removed Aldor support
(which almost nobody used) and got chastised. I removed Boot (since
only half a dozen people speak it) and started a major revolt. Now I'm
removing SPAD as it can't support the dependent type theory or the
proof hierarchy. Notably, all of the things I removed had no effect on
Axiom's ability to compute.
The new top level is lisp. The system is being restructured using CLOS
and the Meta-Object protocol. The algebra is now in a CLOS hierarchy.
Notably, the resulting system will have no effect on Axiom's ability to compute.
PHILOSOPHY
The lisp top-level decision has a philosophical base.
"The language one speaks influences the way one thinks about reality,"
known as the Sapir-Whorf hypothesis [3].
My programming hypothesis I call the "impedence theory". The tools you
use may be closer to the problem (e.g. SPAD) or closer to the solution
(i.e. the hardware, the proof, the algebra, etc.). Most languages are
"high level" and far from the solution so people create their own
language like SPAD to express their ideas. I like to think of this as
"connecting to a fire hydrant with a soda straw". From the full range of
ideas (the hydrant) the language limits what can be thought (the straw).
This is what I call an "intellectual impedence mismatch".
Unfortunately the SPAD straw won't support the new research.
Lisp is the only language I know that does not have the impedence
issue. One can create high level software in perfect cooperation with
machine-level manipulation, e.g. (integrate (car x)).
Nobody, absolutely nobody, will want to use this new Axiom.
TARBALL
>Alternatively, if you would prefer total privacy and/or work on
>something totally different, I'll ensure that the last 20170501 sources
>are preserved for posterity, again free from bit rot. It would be
>helpful if this final released tarball was again available via your
>website.
Point me at the tarball and I'll host it.
>As for github, I'm afraid I do not know (yet) how to add users to
>repositories. I can find out, but we can save ourselves some effort in
>the case that this is not your intended working tree. For example, is
>github in a buildable state at the moment?
Microsoft has made github much more painful to use. I'll see if I
can figure out how to grant you write access.
The github sources mirror my local Axiom tree.
The SANE branch is separate and local.
PAST and FUTURE
>You obviously have accumulated a lot of knowledge and familiarity with
>this great system, which seems to me to be of great value to present and
>future users. As I get older, my thoughts increasingly gravitate toward
>strategies for leaving the fruits of my labors in a form that
>researchers yet to come will find useful. I'm happy to assist with the
>AXIOM legacy in whatever form you choose to leave it.
I've spent approximately 20 years trying to "leave the fruits of (other
people's) labor" in useful form. The community has other goals.
No-one seems to be planning beyond their own local use.
It is easy to see where that will end.
I haven't "left" Axiom. I'm still developing it. It doesn't look the same
but it computes the same. The new version will have a firmer foundation
based on the state of the art in proofs, type theory, and category theory.
I could use a few grad students if you find any to spare :-)
Tim
[2] Christina David, Daniel Kroening, and Matt Lewis
"Unrestricted Termination and Non-Termination Arguments For
AxiomNobodyCares.png