From MAILER-DAEMON Fri Jan 03 02:56:48 2020
Received: from list by lists.gnu.org with archive (Exim 4.90_1)
id 1inHpA-0000bg-F4
for mharc-axiom-developer@gnu.org; Fri, 03 Jan 2020 02:56:48 -0500
Received: from eggs.gnu.org ([2001:470:142:3::10]:49341)
by lists.gnu.org with esmtp (Exim 4.90_1)
(envelope-from ) id 1inHp6-0000ax-Ea
for axiom-developer@nongnu.org; Fri, 03 Jan 2020 02:56:46 -0500
Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71)
(envelope-from ) id 1inHp4-00022B-9J
for axiom-developer@nongnu.org; Fri, 03 Jan 2020 02:56:44 -0500
Received: from mail-qv1-xf41.google.com ([2607:f8b0:4864:20::f41]:37494)
by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_128_CBC_SHA1:16)
(Exim 4.71) (envelope-from ) id 1inHp3-0001we-W1
for axiom-developer@nongnu.org; Fri, 03 Jan 2020 02:56:42 -0500
Received: by mail-qv1-xf41.google.com with SMTP id f16so15929949qvi.4
for ; Thu, 02 Jan 2020 23:56:41 -0800 (PST)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025;
h=mime-version:in-reply-to:references:from:date:message-id:subject:to
:cc:content-transfer-encoding;
bh=uvtm9OS9oGqGtX7v9EIjVX/UFlsk+03Q3Iqpq2BOxuE=;
b=oPy16ggdLMlYbdyAFoBNcrEAikF5qm27++gArbok+bZe4H5jDFY7rVs71nkscijKQt
Yxpnqg4truJL16Wllpm3fsVwpMqIBjDmL6CTOcbdsKuqJJ0TLXZWBSvzFV7DB83sJgqZ
nGyQZJ9fwfJsRe/9Qf+9bGKVAV420aqZeFo3cxGU2yCH1ghAtqjHGIWXtEqK8VPp/hKt
cUnOgHT09GyKGgGRVyVUDoK0s3QKN5HVfHGaeWYwa87cD9CFOrHL1iZDKsg+kwXcy/0M
x5w8i5Z9oAz1G7hhm9M5j6DchwQ5YhzYKD3XjReCH2MmRKyYTFNdaRimT/1t8EKMWCni
d8nw==
X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
d=1e100.net; s=20161025;
h=x-gm-message-state:mime-version:in-reply-to:references:from:date
:message-id:subject:to:cc:content-transfer-encoding;
bh=uvtm9OS9oGqGtX7v9EIjVX/UFlsk+03Q3Iqpq2BOxuE=;
b=qyOx/ZvCdnelPYP9d0o8M/l/tjggMAh0WNoIFVUM3p2DfJiYtjDsMU82UlLNlCdiwQ
7OintSiPj3RDjzTd57SUrMChh6CfiGkBkGJpH5a973Bt15xfiL4TXWVv+DFRdsVM9PLl
DEquAxz0BT+8P2kl6xGEKhfOB9fPbUrNvr0EOWZzr96MxtsCTAH1Hfs8Nc2oGR674SPz
xn3qmolxS/LJmdT7Fuzu+e8xRiWb4MWYU5x+cFzNjMvFVt0uCrdXqhuNu4aUTxWHL5F8
QM9IUwLo4Ag2+gowta4sllUjYg5ljaq4lJ4C/7UhK+F9PDiWaSt7Xqn6REJiS7Y2T2hw
85ow==
X-Gm-Message-State: APjAAAWSe7CVFWqStiKXk2nb521ERGrrXqtMuIhxuJBTJFLSN4lRO7KF
4G22HikeyVklfi/ahv1w+BR4dcTSSDBO8XqLRiyC+KQn
X-Google-Smtp-Source: APXvYqwRkEI9DbdnN/EgD6HeV6gokBvmmzzWNrlT1xJaXhyVlu0JVRm7iegNOFrT1nNjfCCXTERmKfwOu2afz/aFR5k=
X-Received: by 2002:a05:6214:923:: with SMTP id
dk3mr64405403qvb.96.1578038200312;
Thu, 02 Jan 2020 23:56:40 -0800 (PST)
MIME-Version: 1.0
Received: by 2002:a0c:aa14:0:0:0:0:0 with HTTP;
Thu, 2 Jan 2020 23:56:39 -0800 (PST)
In-Reply-To:
References:
From: Tim Daly
Date: Fri, 3 Jan 2020 02:56:39 -0500
Message-ID:
Subject: Re: Axiom musings...
To: axiom-dev , Tim Daly
Cc: Andrej Bauer , Jeremy Avigad
Content-Type: text/plain; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable
X-detected-operating-system: by eggs.gnu.org: Genre and OS details not
recognized.
X-Received-From: 2607:f8b0:4864:20::f41
X-BeenThere: axiom-developer@nongnu.org
X-Mailman-Version: 2.1.23
Precedence: list
List-Id: Axiom Developers
List-Unsubscribe: ,
List-Archive:
List-Post:
List-Help:
List-Subscribe: ,
X-List-Received-Date: Fri, 03 Jan 2020 07:56:46 -0000
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 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 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 =E2=80=9Ctypes=E2=80=9D
>> 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 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 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-fo=
rmer.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_lan=
guage_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 system=
s
>>>> 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 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 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
>>>>>>>
>>>>
>>>
>>
>
From MAILER-DAEMON Thu Jan 09 17:47:30 2020
Received: from list by lists.gnu.org with archive (Exim 4.90_1)
id 1ipgaQ-0008AS-KD
for mharc-axiom-developer@gnu.org; Thu, 09 Jan 2020 17:47:30 -0500
Received: from eggs.gnu.org ([2001:470:142:3::10]:53555)
by lists.gnu.org with esmtp (Exim 4.90_1)
(envelope-from ) id 1ipgaM-0008AL-Pd
for axiom-developer@nongnu.org; Thu, 09 Jan 2020 17:47:29 -0500
Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71)
(envelope-from ) id 1ipgaK-0001Yh-Do
for axiom-developer@nongnu.org; Thu, 09 Jan 2020 17:47:26 -0500
Received: from mail-qt1-x82f.google.com ([2607:f8b0:4864:20::82f]:38658)
by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_128_CBC_SHA1:16)
(Exim 4.71) (envelope-from ) id 1ipgaK-0001SU-5L
for axiom-developer@nongnu.org; Thu, 09 Jan 2020 17:47:24 -0500
Received: by mail-qt1-x82f.google.com with SMTP id n15so281318qtp.5
for ; Thu, 09 Jan 2020 14:47:23 -0800 (PST)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025;
h=mime-version:in-reply-to:references:from:date:message-id:subject:to
:content-transfer-encoding;
bh=QJhMdzzDL/vxPpoNdWRmEZPZgblnbQCp891BoW4xNwg=;
b=XMR/QDNKgvRkyzbUB0EYZ53ZDbFXyVD30qfvFS7UEV6fK4miO07Eu0u67XlywaaAIJ
M9u475JqDERVLnp5j8TQaGDqPXtHRwzD4iT0Nh6765tr5aqs2XosLopLzC5eXMKx5aSx
Mb2iodv3uw6fi/2MhI2awoFEnphDjL2XNNKMzBiufgybreyufZUYQ3K83qMhgLFbIzwG
pgsp0jxAWew8fTBboFeNCSdj3KnwqNFHhbQuMhOCJNRsQPIPpjlvuxXF3Pab+b4lq77Q
zILoVOVmGSBeZ8K4ksnqwl3vOXYZg7zvGR4UgpP5dIes9L9cHdCd5i0sSQeucdoKLeVT
IwCA==
X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
d=1e100.net; s=20161025;
h=x-gm-message-state:mime-version:in-reply-to:references:from:date
:message-id:subject:to:content-transfer-encoding;
bh=QJhMdzzDL/vxPpoNdWRmEZPZgblnbQCp891BoW4xNwg=;
b=WiHd+SllOj+6CIKx7U8FIRYg94IkwgL1wGqatFu16YZpRcEJ1Mwfetnl4mwjjN82MN
BLiKVz4y+KPvIV+qKrZtnAk2qw2Tebzn3qpxcQk6a0pyXLic6xHEnlTiobS3OtvBjKSQ
P01VtJAP8YciluoyEtItDZx8cU/PLizFow7qabzoDIX4UDtQRu2aWPwLdE79LQmduqH1
yZUCg1TUGU2TIn6bqYPQoRUWsECFas/vqgW6mn3Cm2AFs7W2vYVaJZSZz4ckDnpo+RMq
twNLmae8gjNRx99o0qOyi0TNjFG7+QiyFLAvQePDhsJOfWPrTXCpmCU1YFzRfrWXjCDU
Ewug==
X-Gm-Message-State: APjAAAW1xgL69aU+P2YS67pBtG33gNfrwIXefQ8oc0sH5c1HEkUrry7n
46hxCCl014alBUJTJmsek8fQ4/rKnO6ytwkuzsWEeg==
X-Google-Smtp-Source: APXvYqzPNBql9NYc3D3KR06mxNACI1L292PnOxu3GyymBXZ4bdBJJcj/ysdW6MLW4fyU110dd9APeW/UHn1fsZZkXAs=
X-Received: by 2002:ac8:5402:: with SMTP id b2mr10192362qtq.132.1578610041741;
Thu, 09 Jan 2020 14:47:21 -0800 (PST)
MIME-Version: 1.0
Received: by 2002:a0c:aa14:0:0:0:0:0 with HTTP;
Thu, 9 Jan 2020 14:47:21 -0800 (PST)
In-Reply-To:
References:
From: Tim Daly
Date: Thu, 9 Jan 2020 17:47:21 -0500
Message-ID:
Subject: Re: Axiom musings...
To: axiom-dev , Tim Daly
Content-Type: text/plain; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable
X-detected-operating-system: by eggs.gnu.org: Genre and OS details not
recognized.
X-Received-From: 2607:f8b0:4864:20::82f
X-BeenThere: axiom-developer@nongnu.org
X-Mailman-Version: 2.1.23
Precedence: list
List-Id: Axiom Developers
List-Unsubscribe: ,
List-Archive:
List-Post:
List-Help:
List-Subscribe: ,
X-List-Received-Date: Thu, 09 Jan 2020 22:47:29 -0000
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 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 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 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 =E2=80=9Ctypes=E2=80=9D
>>> 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 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 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-f=
ormer.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_la=
nguage_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 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 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
>>>>>>>>
>>>>>
>>>>
>>>
>>
>
From MAILER-DAEMON Thu Jan 09 18:33:31 2020
Received: from list by lists.gnu.org with archive (Exim 4.90_1)
id 1iphIx-00021t-89
for mharc-axiom-developer@gnu.org; Thu, 09 Jan 2020 18:33:31 -0500
Received: from eggs.gnu.org ([2001:470:142:3::10]:36966)
by lists.gnu.org with esmtp (Exim 4.90_1)
(envelope-from ) id 1iphIt-0001yZ-IN
for axiom-developer@nongnu.org; Thu, 09 Jan 2020 18:33:29 -0500
Received: from Debian-exim by eggs.gnu.org with spam-scanned (Exim 4.71)
(envelope-from ) id 1iphIr-0001p4-3b
for axiom-developer@nongnu.org; Thu, 09 Jan 2020 18:33:27 -0500
Received: from mail-qt1-x843.google.com ([2607:f8b0:4864:20::843]:44845)
by eggs.gnu.org with esmtps (TLS1.0:RSA_AES_128_CBC_SHA1:16)
(Exim 4.71) (envelope-from ) id 1iphIq-0001lx-PY
for axiom-developer@nongnu.org; Thu, 09 Jan 2020 18:33:25 -0500
Received: by mail-qt1-x843.google.com with SMTP id t3so337214qtr.11
for ; Thu, 09 Jan 2020 15:33:24 -0800 (PST)
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025;
h=mime-version:in-reply-to:references:from:date:message-id:subject:to
:content-transfer-encoding;
bh=rJ6tk9Ic+j01SMBWEMs1NrbgLg1hq/xGrgoUPlxhJ44=;
b=bCV2CH85NDixytfKlOQu4jI2vmi5AOUZ1PvWDSvqUlJNLyHizQ+Bzx+DYCIniIscRP
KCTDkTFvQBJbfsFPJ7s9cKEuTEi1+5tEn1L8hzKCyC8dgXm9QIkYgjklGVgpjOaIxh9m
iqpRlc1UxDhupVL8KqD9WUx2/zB0RSoS4N3f+03oacDx5HB6P/kxUvXCBWyYmq4C8X6u
fZSBZyvP7X4KPk4EhagHa6cROGRhiujC3eeaq4Qf0J/n/VsvcE03mmkNgtI5nyXjfNiY
OVYYRIWJernWj7284uQ/SJ5a0t9A4SclTtqUAMU0YIB5QrKWOKUwLk0mP6WiUDevP+ht
J/Vw==
X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed;
d=1e100.net; s=20161025;
h=x-gm-message-state:mime-version:in-reply-to:references:from:date
:message-id:subject:to:content-transfer-encoding;
bh=rJ6tk9Ic+j01SMBWEMs1NrbgLg1hq/xGrgoUPlxhJ44=;
b=Zn1XCU3aGvHQEPCV0Us+hRs5wsAL95rg2So17/TfBGD7F3Si7QvN2zT35T7/vgfBnD
NpRBXLxWNGkyXTX2UcE/V9n29KLgveFrRSSQOarGTaFPN4blZk3FIg0AHPudi4oONgY0
28gs/WRADt9I8kl+wh4QwTajy/x8VssRroWUrYTdW43fwLueK+J75aFrjn9SJ685f5n8
6HJ+BgQHKAGGq5wxKlBP5P2NOxZFZka/1owiSlfyVWLJERXvctkohLsHx1Pfp+iBALTP
zsu6usfyfjE2aCR43kTG01MuPI4X3Z0xb/Agf1Q6iyoJ4ETYRls0yBBjQJGwzhOI/fHe
VkUg==
X-Gm-Message-State: APjAAAWVfsvhq5o/glX2KU4NuDVMtv0855Mgd16mMyVUUiGj5o4zDVLd
loqPL+t6aGrcKTBVfrEhSnaB3zm2gkjkvo6zvKGGZQ==
X-Google-Smtp-Source: APXvYqxxQBCDUkzsNqay0l93rj0VVOHlN1ATQyo+59sGdqGk3M5X/EwymKwvHb8czaV3Ey5RVBOHE9GiJ/iNY6I0qiU=
X-Received: by 2002:ac8:60cd:: with SMTP id i13mr40526qtm.386.1578612803655;
Thu, 09 Jan 2020 15:33:23 -0800 (PST)
MIME-Version: 1.0
Received: by 2002:a0c:aa14:0:0:0:0:0 with HTTP;
Thu, 9 Jan 2020 15:33:22 -0800 (PST)
In-Reply-To:
References:
From: Tim Daly
Date: Thu, 9 Jan 2020 18:33:22 -0500
Message-ID:
Subject: Re: Axiom musings...
To: axiom-dev , Tim Daly
Content-Type: text/plain; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable
X-detected-operating-system: by eggs.gnu.org: Genre and OS details not
recognized.
X-Received-From: 2607:f8b0:4864:20::843
X-BeenThere: axiom-developer@nongnu.org
X-Mailman-Version: 2.1.23
Precedence: list
List-Id: Axiom Developers
List-Unsubscribe: ,
List-Archive:
List-Post:
List-Help:
List-Subscribe: ,
X-List-Received-Date: Thu, 09 Jan 2020 23:33:30 -0000
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 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 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 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 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 =E2=80=9Ctypes=E2=80=9D
>>>> 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 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 wrote:
>>>>>> The underlying technology to use for building such an algebra librar=
y
>>>>>> is
>>>>>> documented in the paper " Building on the Diamonds between Theories:
>>>>>> Theory Presentation Combinators"
>>>>>> http://www.cas.mcmaster.ca/~carette/publications/tpcj.pdf [which wil=
l
>>>>>> 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 i=
s
>>>>>> 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_l=
anguage_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 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 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
>>>>>>>>>
>>>>>>
>>>>>
>>>>
>>>
>>
>