Camm,
The "next generation" of Axiom has a few goals that is significantly
reshaping the whole project. I call the effort SANE (a synonym of
rational, judicious, sound, rational). I gave a talk about it at Notre
Dame a few years ago (pre-covid).
There are two streams of mathematical development that seem to be
related but have only James Davenport in common, at least from my
survey of the last 25 years of publications. One stream is computer
algebra, the other is proof theory (e.g. COQ, LEAN, etc.).
The proof people can't trust the computer algebra stream since, while
some of the algorithms such as Buchberger's Groebner basis have
been proven, most of the computer algebra is ad-hoc.
The computer algebra stream seems unaware of the proof work.
While truly impressive algorithms have been developed they tend to
have the "it works for me" level of test and validation.
MERGING proof and computer algebra
My current effort merges LEAN [0] and Axiom. There is the usual
Axiom hierarchy (category/domain/package) and a parallel hierarchy
containing definitions, theorems, and proofs. Each function in Axiom
inherits from both. This allows Axiom's group theory scaffold to be
placed on proven grounds, usable in the proof of the functions.
(Axiom builds a separate subtree containing all of Axiom's functions
at the moment).
Additionally, the REP representation of the domain is now broken out
into a separate chain since the representation has its own associated
theorems, again usable in the proof of the functions.
Axiom is rather strongly typed but post-IBM development of type
theory has moved to dependent types [1]. This allows for much more
precise type specifications.
DEPENDENT TYPE extensions of Axiom's types
One interesting thing about my type theory efforts in Axiom is that
a type computation can involve all of lisp and other Axiom algorithms.
A dependent type might even be recursive, which raises issues of
finding the fixed point to end the recursion. It is a challenge to
manage the complexity (but endless fun).
That said, since the types express the associated theorems, they
become available for proving functions in the domain. More precise
type information gives better, shorter, and more focused proof trees.
LISP
I've been doing the work using CLOS. I've moved the Axiom
hierarchy into a CLOS class tree format. The top level of Axiom
is now using lisp syntax rather than SPAD. I might put a SPAD
language cover over the whole of it. Currently SPAD doesn't
have the necessary syntax to handle dependent types or logic.
It is hard enough getting things working without worrying about
reworking the compiler to create "syntactic sugar". As Axiom has
shown, a separate compiler / interpreter has subtle issues.
Using lisp as the "top level" has two rather useful effects. First,
the interpreter and compiler are the same so the current Axiom
issue goes away. Second, all of the lisp tools are available and
make sense rather than some random error message from the
Axiom algorithm.
There is also the issue of "trust". I've been working to push the
"trusted code", aka the compiler output "all the way down to the
metal". In the instance, that means pushing the generated code
down to run on an FPGA hardware base that offers support for
the generated code. RISC-V[2] soft core cpu work has made this
much easier. RISC-V allows for "extended instructions" which can
be dynamically defined to support specific workloads (in this case,
Axiom).
The FPGA tool chain for small chips works well. Note that Intel
(which bought Altera) and AMD (which bought Xilinx) have CPUs
which include a native FPGA. Unfortunatly they are only available
to data centers. I expect this to change in the future.
Ultimately the system is designed to be "trusted" from the metal
to the top-level algorithms. I've been experimenting with sending
the proof along with the runtime code. Checking a proof is much
faster and easier than the initial proof. This allows the proof to
run on a separate processor checking the result using the
specific values known at runtime. The idea of "proof carrying
code" is not new but interesting in this new context.
STEELE's book
As an aside, I published a hypertex version of Steele's book a
few years ago. It used to be on my server until someone attacked
and destroyed my server. A copy, with the associated latex sources
is online here [3].
Anyway, I've been thinking of building a new version of the book that
contains things like "pre-conditions", "post-conditions", and "invariants"
for each of the lisp functions. People using lisp could have these
available for program validation.
OPEN SOURCE
Having released Axiom as open source I learned a few lessons.
One is that not everyone agrees with and works toward the
published project goals. Another is that a community is
rather fragile and easily collapsed. A third is that I am not
suited for "management" and should not try to lead a project.
You'll notice that I've stopped updating the Axiom source tree.
I thought FOSS development was a great idea when I started
in 1997. The Axiom effort has convinced me otherwise.
I've stopped working in "open source".
GITHUB
If you know the commands to give you write access I'd be
happy to enable you. Please let me know how.
Again, many thanks for your work.
Tim