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 <axiom...@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 <axiom...@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 >> >