The goal is to prove Axiom algorithms, such as the GCD
over the natural numbers, correct using something like Lean.
I've studied traditional approaches like Hoare triples
but I think there might be a different approach. It depends
on Harper's Trinity.
Suppose I had a set of verification condition
Quoting Dijkstra (1988, EWD1036):
... a program is no more than half a conjecture. The other
half of a conjecture is the functional specification the
program is supposed to satisfy. The programmer's task
is to present such complete conjectures as proven theorems.
Axiom's SANE research project is
I occasionally get grief because Axiom is implemented
in Common Lisp. People don't seem to like that for some
odd reason. Lisp, one of the easiest languages to learn,
seems to be difficult to accept.
I'm working with John Harrison's book "Practical Logic
and Automated Reasoning" from 2009. It uses
__
> From: Axiom-developer
> on behalf of
> Tim Daly
> Sent: Thursday, September 24, 2020 4:26 AM
> To: Ricardo Corral C.
> Cc: axiom-developer@nongnu.org
> Subject: [EXTERNAL] Re: Axiom musings...
>
> Today's Headline:
>
> Axiom finalizing a
From: Axiom-developer
on behalf of Tim
Daly
Sent: Thursday, September 24, 2020 4:26 AM
To: Ricardo Corral C.
Cc: axiom-developer@nongnu.org
Subject: [EXTERNAL] Re: Axiom musings...
Today's Headline:
Axiom finalizing agreements for private astronaut mission to space st
y.cuny.edu
From: Tim Daly
Sent: Saturday, July 25, 2020 5:18 AM
To: William Sit
Cc: axiom-dev
Subject: Re: [EXTERNAL] Re: Axiom musings...
The further I get into this game, the harder it becomes.
For example, equality. In the easiest case Axiom has
propositional equality. That is, th
t;> Too bad we did not continue that effort. Does such a domain (in any
>> computer
>> algebra system) exist these days? After all, nearly three decades have
>> passed.
>>
>> William
>>
>> William Sit
>> Professor Emeritus
>> Department of Mathema
uter
> algebra system) exist these days? After all, nearly three decades have
> passed.
>
> William
>
> William Sit
> Professor Emeritus
> Department of Mathematics
> The City College of The City University of New York
> New York, NY 10031
> homepage: wsit.ccny.cuny.edu
>
__
From: Tim Daly
Sent: Monday, July 20, 2020 4:44 PM
To: William Sit
Cc: axiom-dev
Subject: Re: [EXTERNAL] Re: Axiom musings...
> So there are two kinds of algorithms, one that is purely mathematical
> and one that is computational, the latter including a particular (class o
hm handles overflows correctly AND specified in the documentation.
>
> I am sure I am just being ignorant to pose these questions, because they
> must have been considered and perhaps solved. In that case, please ignore
> them and just tell me so.
>
> William
>
> William Sit
&g
w York
New York, NY 10031
homepage: wsit.ccny.cuny.edu
From: Tim Daly
Sent: Sunday, July 19, 2020 5:33 PM
To: William Sit
Cc: axiom-dev
Subject: Re: [EXTERNAL] Re: Axiom musings...
There are several "problems" with proving programs correct that
I don
h the same rigor since behind every program is an algorithm.
>
> William
>
> William Sit
> Professor Emeritus
> Department of Mathematics
> The City College of The City University of New York
> New York, NY 10031
> homepage: wsit.ccny.cuny.edu
>
> ___
ny.edu
From: Axiom-developer
on behalf of Tim
Daly
Sent: Saturday, July 18, 2020 6:28 PM
To: axiom-dev; Tim Daly
Subject: [EXTERNAL] Re: Axiom musings...
Richard Hamming gave a great talk. "You and Your Research"
https://urldefense.proofpoint.com/v2/url?u=https-3A__www.youtu
13 matches
Mail list logo
