Re: [EXTERNAL] Re: Axiom musings...

[Tim Daly]

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 conditions V.
Suppose I had a functor that carries V to a program P.
Suppose I had a functor that carries V to a proof  Q.
By the category definition of functors this implies a
natural transformation between P and Q ... and I'm done.

Except for some annoying details, of course.

1) What is a functor from V to P? Well, I have all of
group theory already available because of the way
Axiom is constructed. So the "elements" of the functor
requires things like "carrying identity". Exactly what
this implies in the constructed program P needs to
be worked out in detail.

2) What is the functor from V to Q? Well, if I construct
a sequent calculus version of Lean's Type Theory then
I have a "complete" set of low-level tactics. It isn't clear
how those tactics can be applied to construct the functor
(at least not yet).

3) The two functors require certain constraints on the
verification conditions V. In dealing with the GCD over
the natural numbers (known as NonNegativeInteger or
NNI in Axiom) we need to make sure that V contains
all of the conditions that the correct program requires
(such as deriving the recursive call).

4) V also needs constraints in dealing with the GCD
so that the proof can use the Lean sequent rules
to derive a proof of the GCD. So I'd have to construct
a sequent proof of the GCD from the sequent-derived
tactics.

5) I don't know of a languge V that covers both the
needs of the functors for P and Q so that will take
some omphaloskepsis. I might have to write a
"linter" program.

This category theory approach, using Harper's Trinity,
has the potential of proving programs correct without
dealing with things like Hoare triples.

This all works in theory but there is a lot of practical
work, such as deriving a sequent form of Lean's Type
Theory, deriving functors that fulfill all the definitions
using things like Axiom's group theory structure, and
inventing the verification language V rich enough
for both needs.

It's gonna be a long winter :-)

Tim
.

On 12/18/20, Tim Daly <axiomcas@gmail.com> wrote:
> 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 trying to build a system
> where such "complete conjectures as proven theorems"
> can be implemented, at least for mathematical algorithms.
>
> After 50 years of programming it is humbling to realize
> that I've neglected the most important half of programming.
>
> The amount of effort and progress in proof theory, category
> theory, and interactive theorem proving is amazing; most
> of it only occuring in this century. I've spent the last 8 years
> trying to "catch up" with what future programmers will take
> as normal and expected.
>
> Imagine a Google whiteboard interview where you are
> asked to provide an algorithm and an associated proof.
> Will you get hired?
>
> Dijkstra saw this in 1988 and it's taken me decades to
> hear and understand.
>
> Tim
>
>
> On 12/18/20, Tim Daly <axiomcas@gmail.com> wrote:
>> 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 OCaml
>> to implement the programs.
>>
>> I've downloaded the OCaml sources from the website.
>> Apparently OCaml has changed significantly from 2009
>> since the code no longer compiles, spitting out "Alert
>> deprecated" all over the place and simply failing in places.
>>
>> C++ code has a "standard", well, several "standards".
>> When someone asks "Do you know C++" you really
>> need to qualify that question. What you knew about
>> "standard C++" seems to change every 2 years.
>>
>> I recently pulled out my KROPS code, used as the
>> basis for IBM's Expert System FAME. It was written
>> in Common Lisp (on a Symbolics machine). It still runs
>> unmodified despite being written about 40 years ago
>> on hardware and a software stack that no longer exists.
>>
>> Axiom, written in the last century, still compiles and
>> runs. Say what you want about Lisp code, it still is the
>> most portable and long-lasting language I've ever used.
>>
>> Tim
>>
>