One major Sane design decision is the use of CLOS,
the Common Lisp Object System.
First, since each CLOS object is a type it is possible to
create strong types everywhere. This helps with the ultimate
need to typecheck the compiler and the generated code.
Second, CLOS is an integral part of common lisp. One of
the Sane design goals is to make it possible to use Axiom's
domains in ordinary lisp programs. Since Axiom is nothing
more than a domain specific language on common lisp it
makes sense to construct it so users can freely intermix
polynomials with non-algebraic code.
Third, CLOS is designed for large program development,
hiding most of the implementation details and exposing
a well-defined API. This will make future maintenance and
documentation of Axiom easier, contributing to its longer
intended life.
So for a traditional Axiom user nothing seems to have
changed. But for future users it will be easy to compute
an integral in the middle of regular programs.
Tim
On 6/27/19, Tim Daly <address@hidden> wrote:
Another thought....
There has been a "step change" in computer science in the last few years.
Guy Steele did a survey of the use of logic notation in conference papers.
More than 50% of the papers in some conferences use logic notation
(from one of the many logics).
CMU teaches their CS courses all based on and requiring the use of
logic and the associated notation. My college mathematics covered
the use of truth tables. The graduate course covered the use of
Karnaugh maps.
Reading current papers, I have found several papers with multiple
pages containing nothing but "judgements", pages of greek notation.
If you think Axiom's learning curve is steep, you should look at
Homotopy Type Theory (HoTT).
I taught a compiler course at Vassar in the previous century but
the Dragon book didn't cover CIC in any detail and I would not
have understood it if it did.
The original Axiom software predates most of the published logic
papers, at least as they applied to software. Haskell Curry wrote
from the logic side in 1934 and William Howard published in 1969
but I only heard of the Curry-Howard correspondence in 1998.
Writing a compiler these days requires the use of this approach.
In all, that's a good thing as it makes it clear how to handle types
and how to construct software that is marginally more correct.
The new Sane compiler is building on these logic foundations,
based on the Calculus of Inductive Construction and Dependent
Type theory. The compiler itself is strongly typed as is the
language it supports.
Since dependent types are not decidable there will always be
heuristics at runtime to try to disambiguate types, only now we
will have to write the code in greek :-)
Tim