Re: [Axiom-developer] [EXTERNAL] Re: Axiom's Sane redesign musings

[Tim Daly]

There are thousands of hours of expertise and thousands of
functions embedded in Spad code. An important design goal
is to ensure that code continues to function. The Sane compiler
will output code that runs in the interpreter. It is important that
"nothing breaks".

That said, the Sane compiler is "layered". The core of the design
is that Axiom categories, domains, and packages are represnted
as lisp classes and instances. This "core" is essentially what the
compiler people call an Abstract Syntax Tree (AST). But in this
case it is much more than syntax.

Given this "core" there are several tasks.

1) compile spad code to the core. The "front end" should
accept and understand current Spad code, unwinding it
into the core class structure.

2) compile core classes to Axiom data structures. Thi
"back end" generates current Axiom data structures from
the core data structures.

Now the compiler generates working code yet is in a state
to accept enhancements, essentially by extending the core
class objects.

3) In the interpreter, modify the getdatabase function to
extract data from the core rather than the databases. So
the databases go away but the interpreter continues to work.

So now the interpreter has been "lifted" onto the core classes
but continues to function.

4) enhance the core to support the axioms / specifications /
proofs /etc. This involves adding fields to the lisp classes.
This core work gives additional fields to hold information.

5) extend the Spad language (Spad 2.0?) to handle the
additional axioms / specifications / proofs / etc. This
involves adding syntax to the Spad language to support
the new fields.

6) build back-end targets to proof systems, spec systems,
etc. Compilers like GCC have multiple back ends. The Sane
compiler targets the interpreter, a specification checker, a
proof system, etc. as separate back ends, all from the same
core structures.

The Compiler Design

A separate but parallel design goal is to build the compiler so
it can be type-checked. Each function has typed input and
typed output and is, for the most part, purely functional. So,
for example, a "Filename" is an instance of a "File" object.
A "Line" is an instance of "String". The "FileReader" is

FileReader : Filename -> List Line

Careful design of the language used to construct hte compiler
(as opposed to the Spad language it accepts) makes it easier
to type check the compiler itself.

By REALLY careful design, the types are build on a layered
subset of lisp, like Milawa
https://www.cl.cam.ac.uk/~mom22/soundness.pdf
which is sound all the way down to the metal.

It all goes in stages. Build the new core class structure in a
strongly typed fashion. Accept the Spad language. Generate
Interpreter code. Enhance the core to support proofs / specs.
Enhance the language to support proofs / specs. Accept the
new language. Generate back ends to target the interpreter
and a proof / spec system. Build it all on a sound base so
the compiler can be checked.

To the initial end user, the Sane version is the same as the
current system. But in the long term all of the Axiom code
could be called from any Lisp function. The Sane version
can also be used as an "Oracle" for proof systems, since
the code has been proven correct.

This is a huge project but it can be done in small steps.
In particular, the goal is to build a "thin thread" all the way
through the system to handle only the GCD algorithms.
Once that proof happens "the real work begins".

Tim




On 6/30/19, Martin Baker <address@hidden> wrote:
> Tim,
>
> This all seems to be about the lisp layer, obviously thats what
> interests you.
>
> It seems to me that if SPAD code is complicated and not aligned to type
> theory then, when SPAD is complied to Lisp, the List code will be
> complicated and hard to work with. Your previous remarks, about not
> seeing the whole elephant, suggest to me that you are drowning in
> complexity. Most languages, in their lifetime, acquire some messiness
> that needs to be cleared out occasionally.
>
> Don't you think its time for SPAD 2.0 ?
>
> Martin
>
> On 30/06/2019 02:17, Tim Daly wrote:
>> 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
>