I originally shared this just under two years ago, but I want to resubmit it again. Why? Because in the time since the last submission, we went from seven proofs of leftpad to 17! You can now compare Agda’s proof style to ACL2, see how to formally prove Java correct, and even read a proof for an FPGA process!
People are, of course, welcome to submit proofs for languages not yet present.
Stories with similar links:
- Let's Prove Leftpad authored by hwayne 4 years ago | 29 points | 8 comments
The twitter thread for this was the first time I heard of you, Hillel (I think that you also proposed other programs to be proven, in addition to leftpad? Edit: There it is!). Since then I’ve been reading many of your posts.
I recently tried to do a pen-and-paper proof of a bubble sort, and see if and how this could be formalized. The context is “Suppose you’d made a programming language in which proving programs correct is as close as possible to what a mathematician would do on paper”. My experiences:
I choose to use functions to model arrays. An int array with n elements becomes a function from { 0, 1, …, n - 1 } to the integers. Now, we can phrase the requirement for a sorting function that the output function/array equals the composition of a permutation of { 0, 1, …, n - 1 } and the input function. Now you need some theory on permutations (most relevant: if you swap two elements in a permutation, it’s still a permutation).
On top of that, you also need some axioms for integers. With these techniques and with a lot of loop invariants, it’s possible to prove the correctness of bubble sort. Then you realize you’ll also need to prove termination…
Nothing in these steps is prohibitively hard, but it’s a lot of work and quite a rabbit hole!
Just to throw it out there since I got nerdsniped, are the following criteria not enough to express “contains the same elements”?
Maybe one or both of those criteria is itself hard to express.
If the input contains duplicates, the output could contain another element and still fulfil those requirements.
You could hane it apply to both in->out and out->in. but but then the same thing could happen if there’s more than one element that has duplicates.
Ah! Yep, I see it now. Thanks!
@kyrias pointed out the issue, but you can make this valid by instead saying “every element of the input has the same count in the output.” In fact when I teach workshops I have students specify sorting both ways, as a permutation spec and as a counter spec.
This is a great repo!
Idris really shines here, as does the java & smt example - none of which I ever would have thought about even trying. These comparative things can lead to dumb stuff, but for me it’s really great to see things that are not spark or coq.
I learnt some Idris and really liked it. Based on https://whatisrt.github.io/dependent-types/2020/02/18/agda-vs-coq-vs-idris.html I decided to spend some effort to learn Agda. It was far from trivial to set up and takes very long to compile. So far I’m not impressed (but I so far I have only spent one evening, so I only just started).
FWIW: https://github.com/lemmy/lets-prove-blocking-queue/ is the sequel to Let’s Prove Leftpad with a focus on concurrency.