I did the Peano gig for the Edinburgh DReaMers. It was great to meet J Moore there, and he got interested enough to bang out a proof of binPeano with ACL2, in double quick time. His proof goes in three easy stages:
(more…)
Last Friday, shortly after my return from Edinburgh, I gave a slappably smug talk, in an infuriating up-the-garden-path style, about an idea which was provoked by James McKinna, and by which I was somewhat tickled. It’s an exploration of the freedom you get with dependent types to shift where you draw the line between building hygiene conditions into the structure of your data, thus preventing certain kinds of error a priori, and verifying that your programs satisfy laws a posteriori.
James reminded me of the compiler correctness story (McKinna and Wright, to appear in JFP). He and Joel showed how to compile a simple expression language into ‘bytecode’ for a stack machine. The datatype of code guaranteed operand compatibility and prevented underflow, making it easier to give its semantics. The proof that the compiled code was correct with respect to the evaluation function was done later. James asked me what would happen if we tried to build compiler correctness, not just stack safety, into the types. Guess what…?
(more…)
This is a story from the early days of designing Epigram. It’s a case study of equipping a data structure with a funny induction principle. I want to show that a binary representation of positive numbers satisfies a unary induction principle. I think I got the problem from Nicolas Magaud a while back, but Hugo Herbelin reminded me of it at CHIT/CHAT, so I dug it out of my bottom drawer. I’ll be informal, tending to Agda, notationally.
Positive binary numbers are snoc-lists of bits with a 1 at the front.
We can easily write their successor operation by structural recursion.
Now the task is to give
I’ll give a broken attempt, followed by my proof, and then James McKinna’s proof.
(more…)