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
No, the name 'Axiom" is used by many different companies.
Trademarks only cover infringement "in the same area"
(although the Lexus car company sued a diner named
Lexus and "won" because the diner couldn't compete
against big corporate lawyer money).
One company in New Jersey named their language
Axiom Space, a Houston-based company, is not related to Axiom the scientific
computation system. Or is it?
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
___
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
There are several "problems" with proving programs correct that
I don't quite know how to solve, or even approach. But that's the
fun of "research", right?
For the data representation question I've been looking at types.
I took 10 courses at CMU. I am eyebrow deep in type theory.
I'm looking at ca
Hi Tim:
Glad to hear from you now and then, promoting and working towards your ideas
and ideals.
>>We need proven algorithms.
Just one short comment: it is often possible to prove algorithms (that is,
providing the theoretical foundation for the algorithm), but it is much harder
to prove tha
13 matches
Mail list logo
