Re: Axiom musings...

[Tim Daly]

As a mathematician, it is difficult to use a system like Axiom,
mostly because it keeps muttering about Types. If you're not
familiar with type theory (most mathematicians aren't) then it
seems pointless and painful.

So Axiom has a steep learning curve.

As a mathematician with an algorithmic approach, it is difficult
to use a system like Axiom, mostly because you have to find
or create "domains" or "packages", understand categories
with their inheritance model, and learn a new language with
a painful compiler always complaining about types.

So Axiom has a steep learning curve.

The Sane version of Axiom requires knowing the mathematics.
It also assumes a background in type theory, inductive logic,
homotopy type theory, ML (meta-language, not machine
learning (yet)), interactive theorem proving, kernels, tactics,
and tacticals. Also assumed is knowledge of specification languages,
Hoare triples, proof techniques, soundness, and completeness.
Oh, and there is a whole new syntax and semantics added to
specify definitions, axioms, and theorems, not to mention whole
libraries of the same.

So Axiom Sane has a steep learning curve.

I've taken 10 courses at CMU and spent the last 4-5 years
learning to read the leading edge literature (also known
as "greek studies", since every paper has pages of greek).

I'm trying to unify computer algebra and proof theory into a
"computational mathematics" framework. I suspect that the only
way this system will ever be useful is after Universities have a
"Computational Mathematics" major course of study and degree.

Creating a new department is harder than creating Axiom Sane
because, you know, ... people.

I think such a department is inevitable given the deep and wide
impact of computers, just not in my lifetime. That's ok. When I
started programming there was no computer science degree.

Somebody has to be the first lemming over the cliff.

Tim

On 1/9/20, Tim Daly <address@hidden> wrote:
> When Axiom Sane is paired with a proof checker (e.g. with Lean)
> there is a certain amount of verification that is involved.
>
> Axiom will provide proofs (presumably validated by Lean) for its
> algorithms. Ideally, when a computation is requested from Lean
> for a GCD, the result as well as a proof of the GCD algorithm is
> returned. Lean can the verify that the proof is valid. But it is
> computationally more efficient if Axiom and Lean use a cryptographic
> hash, such as SHA1. That way the proof doesn't need to be
> 'reproven', only a hash computation over the proof text needs to
> be performed. Hashes are blazingly fast. This allows proofs to be
> exchanged without re-running the proof mechanism. Since a large
> computation request from Lean might involve many algorithms
> there would be considerable overhead to recompute each proof.
> A hash simplifies the issue yet provides proof integrity.
>
> Tim
>
>
> On 1/9/20, Tim Daly <address@hidden> wrote:
>> Provisos.... that is, 'formula SUCH pre/post-conditions'
>>
>> A computer algebra system ought to know and ought to provide
>> information about the domain and range of a resulting formula.
>> I've been pushing this effort since the 1980s (hence the
>> SuchThat domain).
>>
>> It turns out that computing with, carrying, and combining this
>> information is difficult if not impossible in the current system.
>> The information isn't available and isn't computed. In that sense,
>> the original Axiom system is 'showing its age'.
>>
>> In the Sane implementation the information is available. It is
>> part of the specification and part of the proof steps. With a
>> careful design it will be possible to provide provisos for each
>> given result that are carried with the result for use in further
>> computation.
>>
>> This raises interesting questions to be explored. For example,
>> if the formula is defined over an interval, how is the interval
>> arithmetic handled?
>>
>> Exciting research ahead!
>>
>> Tim
>>
>>
>>
>> On 1/3/20, Tim Daly <address@hidden> wrote:
>>> Trusted Kernel... all the way to the metal.
>>>
>>> While building a trusted computer algebra system, the
>>> SANE version of Axiom, I've been looking at questions of
>>> trust at all levels.
>>>
>>> One of the key tenets (the de Bruijn principle) calls for a
>>> trusted kernel through which all other computations must
>>> pass. Coq, Lean, and other systems do this. They base
>>> their kernel  on logic like the Calculus of Construction or
>>> something similar.
>>>
>>> Andrej Bauer has been working on a smaller kernel (a
>>> nucleus) that separates the trust from the logic. The rules
>>> for the logic can be specified as needed but checked by
>>> the nucleus code.
>>>
>>> I've been studying Field Programmable Gate Arrays (FPGA)
>>> that allow you to create your own hardware in a C-like
>>> language (Verilog). It allows you to check the chip you build
>>> all the way down to the transistor states. You can create
>>> things as complex as a whole CPU or as simple as a trusted
>>> nucleus. (youtube: Building a CPU on an FPGA). ACL2 has a
>>> history of verifying hardware logic.
>>>
>>> It appears that, assuming I can understand Bauers
>>> Andromeda system, it would be possible and not that hard
>>> to implement a trusted kernel on an FPGA the size and
>>> form factor of a USB stick.
>>>
>>> Trust "down to the metal".
>>>
>>> Tim
>>>
>>>
>>>
>>> On 12/15/19, Tim Daly <address@hidden> wrote:
>>>> Progress in happening on the new Sane Axiom compiler.
>>>>
>>>> Recently I've been musing about methods to insert axioms
>>>> into categories so they could be inherited like signatures.
>>>> At the moment I've been thinking about adding axioms in
>>>> the same way that signatures are written, adding them to
>>>> the appropriate categories.
>>>>
>>>> But this is an interesting design question.
>>>>
>>>> Axiom already has a mechanism for inheriting signatures
>>>> from categories. That is, we can bet a plus signature from,
>>>> say, the Integer category.
>>>>
>>>> Suppose we follow the same pattern. Currently Axiom
>>>> inherits certain so-called "attributes", such as ApproximateAttribute,
>>>> which implies that the results are only approximate.
>>>>
>>>> We could adapt the same mechnaism to inherit the Transitive
>>>> property by defining it in its own category. In fact, if we
>>>> follow Carette and Farmer's "tiny theories" architecture,
>>>> where each property has its own inheritable category,
>>>> we can "mix and match" the axioms at will.
>>>>
>>>> An "axiom" category would also export a function. This function
>>>> would essentially be a "tactic" used in a proof. It would modify
>>>> the proof step by applying the function to the step.
>>>>
>>>> Theorems would have the same structure.
>>>>
>>>> This allows theorems to be constructed at run time (since
>>>> Axiom supports "First Class Dynamic Types".
>>>>
>>>> In addition, this design can be "pushed down" into the Spad
>>>> language so that Spad statements (e.g. assignment) had
>>>> proof-related properties. A range such as [1..10] would
>>>> provide explicit bounds in a proof "by language definition".
>>>> Defining the logical properties of language statements in
>>>> this way would make it easier to construct proofs since the
>>>> invariants would be partially constructed already.
>>>>
>>>> This design merges the computer algebra inheritance
>>>> structure with the proof of algorithms structure, all under
>>>> the same mechanism.
>>>>
>>>> Tim
>>>>
>>>> On 12/11/19, Tim Daly <address@hidden> wrote:
>>>>> I've been reading Stephen Kell's (Univ of Kent
>>>>> https://www.cs.kent.ac.uk/people/staff/srk21/) on
>>>>> Seven deadly sins of talking about “types”
>>>>> https://www.cs.kent.ac.uk/people/staff/srk21//blog/2014/10/07/
>>>>>
>>>>> He raised an interesting idea toward the end of the essay
>>>>> that type-checking could be done outside the compiler.
>>>>>
>>>>> I can see a way to do this in Axiom's Sane compiler.
>>>>> It would be possible to run a program over the source code
>>>>> to collect the information and write a stand-alone type
>>>>> checker. This "unbundles" type checking and compiling.
>>>>>
>>>>> Taken further I can think of several other kinds of checkers
>>>>> (aka 'linters') that could be unbundled.
>>>>>
>>>>> It is certainly something to explore.
>>>>>
>>>>> Tim
>>>>>
>>>>>
>>>>> On 12/8/19, Tim Daly <address@hidden> wrote:
>>>>>> The Axiom Sane compiler is being "shaped by the hammer
>>>>>> blows of reality", to coin a phrase.
>>>>>>
>>>>>> There are many goals. One of the primary goals is creating a
>>>>>> compiler that can be understood, maintained, and modified.
>>>>>>
>>>>>> So the latest changes involved adding multiple index files.
>>>>>> These are documentation (links to where terms are mentioned
>>>>>> in the text), code (links to the implementation of things),
>>>>>> error (links to where errors are defined), signatures (links to
>>>>>> the signatures of lisp functions), figures (links to figures),
>>>>>> and separate category, domain, and package indexes.
>>>>>>
>>>>>> The tikz package is now used to create "railroad diagrams"
>>>>>> of syntax (ala, the PASCAL report). The implementation of
>>>>>> those diagrams follows immediately. Collectively these will
>>>>>> eventually define at least the syntax of the language. In the
>>>>>> ideal, changing the diagram would change the code but I'm
>>>>>> not that clever.
>>>>>>
>>>>>> Reality shows up with the curent constraint that the
>>>>>> compiler should accept the current Spad language as
>>>>>> closely as possible. Of course, plans are to include new
>>>>>> constructs (e.g. hypothesis, axiom, specification, etc)
>>>>>> but these are being postponed until "syntax complete".
>>>>>>
>>>>>> All parse information is stored in a parse object, which
>>>>>> is a CLOS object (and therefore a Common Lisp type)
>>>>>> Fields within the parse object, e.g. variables are also
>>>>>> CLOS objects (and therefore a Common Lisp type).
>>>>>> It's types all the way down.
>>>>>>
>>>>>> These types are being used as 'signatures' for the
>>>>>> lisp functions. The goal is to be able to type-check the
>>>>>> compiler implementation as well as the Sane language.
>>>>>>
>>>>>> The parser is designed to "wrap around" so that the
>>>>>> user-level output of a parse should be the user-level
>>>>>> input (albeit in a 'canonical" form). This "mirror effect"
>>>>>> should make it easy to see that the parser properly
>>>>>> parsed the user input.
>>>>>>
>>>>>> The parser is "first class" so it will be available at
>>>>>> runtime as a domain allowing Spad code to construct
>>>>>> Spad code.
>>>>>>
>>>>>> One plan, not near implementation, is to "unify" some
>>>>>> CLOS types with the Axiom types (e.g. String). How
>>>>>> this will happen is still in the land of design. This would
>>>>>> "ground" Spad in lisp, making them co-equal.
>>>>>>
>>>>>> Making lisp "co-equal" is a feature, especially as Spad is
>>>>>> really just a domain-specific language in lisp. Lisp
>>>>>> functions (with CLOS types as signatures) would be
>>>>>> avaiable for implementing Spad functions. This not
>>>>>> only improves the efficiency, it would make the
>>>>>> BLAS/LAPACK (see volume 10.5) code "native" to Axiom.
>>>>>> .
>>>>>> On the theory front I plan to attend the Formal Methods
>>>>>> in Mathematics / Lean Together conference, mostly to
>>>>>> know how little I know, especially that I need to know.
>>>>>> http://www.andrew.cmu.edu/user/avigad/meetings/fomm2020/
>>>>>>
>>>>>> Tim
>>>>>>
>>>>>>
>>>>>>
>>>>>> On 11/28/19, Jacques Carette <address@hidden> wrote:
>>>>>>> The underlying technology to use for building such an algebra
>>>>>>> library
>>>>>>> is
>>>>>>> documented in the paper " Building on the Diamonds between Theories:
>>>>>>> Theory Presentation Combinators"
>>>>>>> http://www.cas.mcmaster.ca/~carette/publications/tpcj.pdf [which
>>>>>>> will
>>>>>>> also be on the arxiv by Monday, and has been submitted to a
>>>>>>> journal].
>>>>>>>
>>>>>>> There is a rather full-fledged prototype, very well documented at
>>>>>>> https://alhassy.github.io/next-700-module-systems/prototype/package-former.html
>>>>>>>
>>>>>>> (source at https://github.com/alhassy/next-700-module-systems). It
>>>>>>> is
>>>>>>> literate source.
>>>>>>>
>>>>>>> The old prototype was hard to find - it is now at
>>>>>>> https://github.com/JacquesCarette/MathScheme.
>>>>>>>
>>>>>>> There is also a third prototype in the MMT system, but it does not
>>>>>>> quite
>>>>>>> function properly today, it is under repair.
>>>>>>>
>>>>>>> The paper "A Language Feature to Unbundle Data at Will"
>>>>>>> (https://alhassy.github.io/next-700-module-systems/papers/gpce19_a_language_feature_to_unbundle_data_at_will.pdf)
>>>>>>>
>>>>>>> is also relevant, as it solves a problem with parametrized theories
>>>>>>> (parametrized Categories in Axiom terminology) that all current
>>>>>>> systems
>>>>>>> suffer from.
>>>>>>>
>>>>>>> Jacques
>>>>>>>
>>>>>>> On 2019-11-27 11:47 p.m., Tim Daly wrote:
>>>>>>>> The new Sane compiler is also being tested with the Fricas
>>>>>>>> algebra code. The compiler knows about the language but
>>>>>>>> does not depend on the algebra library (so far). It should be
>>>>>>>> possible, by design, to load different algebra towers.
>>>>>>>>
>>>>>>>> In particular, one idea is to support the "tiny theories"
>>>>>>>> algebra from Carette and Farmer. This would allow much
>>>>>>>> finer grain separation of algebra and axioms.
>>>>>>>>
>>>>>>>> This "flexible algebra" design would allow things like the
>>>>>>>> Lean theorem prover effort in a more natural style.
>>>>>>>>
>>>>>>>> Tim
>>>>>>>>
>>>>>>>>
>>>>>>>> On 11/26/19, Tim Daly <address@hidden> wrote:
>>>>>>>>> The current design and code base (in bookvol15) supports
>>>>>>>>> multiple back ends. One will clearly be a common lisp.
>>>>>>>>>
>>>>>>>>> Another possible design choice is to target the GNU
>>>>>>>>> GCC intermediate representation, making Axiom "just
>>>>>>>>> another front-end language" supported by GCC.
>>>>>>>>>
>>>>>>>>> The current intermediate representation does not (yet)
>>>>>>>>> make any decision about the runtime implementation.
>>>>>>>>>
>>>>>>>>> Tim
>>>>>>>>>
>>>>>>>>>
>>>>>>>>> On 11/26/19, Tim Daly <address@hidden> wrote:
>>>>>>>>>> Jason Gross and Adam Chlipala ("Parsing Parses") developed
>>>>>>>>>> a dependently typed general parser for context free grammar
>>>>>>>>>> in Coq.
>>>>>>>>>>
>>>>>>>>>> They used the parser to prove its own completeness.
>>>>>>>>>>
>>>>>>>>>> Unfortunately Spad is not a context-free grammar.
>>>>>>>>>> But it is an intersting thought exercise to consider
>>>>>>>>>> an "Axiom on Coq" implementation.
>>>>>>>>>>
>>>>>>>>>> Tim
>>>>>>>>>>
>>>>>>>
>>>>>>
>>>>>
>>>>
>>>
>>
>