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 [0] LEAN https://leanprover-community.github.io/ [1] Dependent Types: https://en.wikipedia.org/wiki/Dependent_type [2] RISC-V https://riscv.org/ [3] Hyperlinked Steele's book: https://www.softwarepreservation.org/projects/LISP/common_lisp_family On Mon, Feb 13, 2023 at 9:38 AM Camm Maguire <c...@maguirefamily.org> wrote: > Greetings! > > Tim, is it your intention that github serves as the official repository > henceforward? Are you intending to tag releases here, and/or push > tarballs to the website? Debian axiom is using sources from 20170501, > which were available back then in tar form but seem to be gone now. Are > you planning any further releases? > > It seems your goals are very ambitious. It may be worthwhile making > sure the tree is periodically and incrementally kept up to date and > releasable as you move forward, say once a year or so. If you would > like to grant me access to the tree (github id cammgh), I can volunteer > to maintain the gcl interface if desired. > > Take care, > -- > Camm Maguire c...@maguirefamily.org > ========================================================================== > "The earth is but one country, and mankind its citizens." -- Baha'u'llah >