Re: Axiom musings...

[Tim Daly]

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
>>>>>>>>>
>>>>>>
>>>>>
>>>>
>>>
>>
>