Re: Axiom git

[Camm Maguire]

Greetings!  What a comprehensive tour de force!

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.

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. 

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.

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.

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?

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.

Take care,

Tim Daly <axiomcas@gmail.com> writes:

> 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 <camm@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                                        camm@maguirefamily.org
>  ==========================================================================
>  "The earth is but one country, and mankind its citizens."  --  Baha'u'llah
>

-- 
Camm Maguire                                        camm@maguirefamily.org
==========================================================================
"The earth is but one country, and mankind its citizens."  --  Baha'u'llah