axiom-developer
[Top][All Lists]
Advanced

[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: Axiom musings...


From: Tim Daly
Subject: Re: Axiom musings...
Date: Thu, 1 Oct 2020 15:32:17 -0400

Hill Climbing....

Almost every possible step along the path to creating
the SANE version of Axiom involves a LOT of hill
climbing, by that I mean a LOT to learn to get started.

Axiom was built with a scaffold of group theory which
makes it easier to reason about and understand. Going
forward we need to use the theories we have learned
since the 1980s to ground the system properly.

One hill is that there is almost no documentation or even
literature reference for many of Axiom's algorithms. Some
were done as PhD research; many were ad-hoc "it works
for me", etc. Axiom already has decorated some of the
algorithms with literature references. More needs to be done.

As for hills, there is the large area of logic which has
many different branches. One has to crawl from one
corner of the lambda cube to the other in order to know
what dependent types are and how to use them.
https://www.cs.uoregon.edu/research/summerschool/summer12/curriculum.html

Then there is the category theory area since we would
like to have things like definitionally correct functors.
https://www.youtube.com/watch?v=Y5YCE_mVjvg&list=PLhgq-BqyZ7i7MTGhUROZy3BOICnVixETS

Then there is the whole area of proof. Currently Axiom
is focusing on Lean as the underlying machinery as it
seems to be the leading edge in constructive type theory
and mathematics.
https://leanprover.github.io

There are many different approaches to specification
ranging from "hand waving" (UML) to strong theory.
But transitioning from the specification to the code is
still a huge gap.
https://formal.iti.kit.edu/~beckert/teaching/Spezifikation-SS04/11Z.pdf

Programming has also advanced. Clojure has raised
some significant issues of concurrent and scalable
programming. It would be great if matrix algorithms
could be run in parallel.
https://clojure.org/about/concurrent_programming

Symbolic-Numeric programming has been an issue.
There is every reason for numeric programs to have a
"place at the table" in a computational mathematics
system. There are interesting issues that arise.
https://www.amazon.com/End-Error-Computing-Chapman-Computational/dp/1482239868

Of course, none of this gets anywhere near the issues
of proving programs correct, that being the central
question.

Then there is the question of creating a compiler that
uses and integrates all of the above as well as being
able to handle the current Axiom algorithms. But the
compiler needs to also recognize and propagate the
logical definitions and axioms along the inheritance
paths.

Of course, the compiler and interpreter should have the
same semantics and work on the same data structures
so that what compiles will interpret and what interprets
compiles.

That doesn't even mention the supposedly trivial issue
of replacing the front end, hyperdoc, and graphics with
a portable browser interface. CSS seems to be a whole
career skill at this point. Plus it really should work well
in the whole "workbook" environment like CoCalc.

Progress is being made in all of these areas but, as
you can imagine, it takes a lot of thought to combine
them cleanly.

Tim



reply via email to

[Prev in Thread] Current Thread [Next in Thread]