Latest Shiny Geek Toy: coq

So, one of the reasons I've been a bit uncommunicative the last few weeks is that I've been getting my head around Coq, maybe one of the most fascinating pieces of software I've played with in a long time.

What is Coq? I don't know if I understand it well enough yet to give a complete description (the Coq tome only arrived in the mail on Friday and I have yet to make it past the introduction, what with taxes and so on). Here's my best shot:

Coq is a programming language where you write proofs as functions taking proofs of their preconditions and producing proofs of their results. That is, a proof that "If X is an integer, then X-1 < X" becomes a function that accepts a proof of "X is an integer" and produces a proof of "X-1 < X".

You can manipulate logical expressions more or less the way you expect. For instance, if you have in your hands a set S of natural numbers and a proof that "forall nonempty sets T of naturals, T has a least element", then you can bang these together to produce the least element of S (or rather, a proof that it exists).

I don't think this describes the theoretical underpinnings of Coq, but it does describe my experience of actually using it to prove stuff.

To get the hang of Coq, I'm working my way through basic automata theory -- regexps are done, but I couldn't work out how to express some finiteness constraints on FSMs without generating a lot of extra typing; hopefully the Coq book will have some hints. Once that's done, I'm actually tempted to try something more ambitious. [snip long digression] We'll see ... watch this space :).

It was a real rush, though, to code up these theorems and watch the computer verify them. What really fascinated me was how close to being a practical tool this is. Coq isn't at all a toy -- without quite getting all the theory yet, my intuition is that it can probably cover anything you can express in the predicate calculus (with sufficient amounts of typing, anyway), and while there are a few shortcomings, it's almost (IMO) at the point where anyone who knows some formal logic and has a little patience can prove interesting stuff. Even more suggestive of possibilities, there's a project (which I sadly haven't had time to look at) that integrates Coq with OCaml, so you can have proofs about your OCaml code verified at compile-time!

I could go on and on ... anyway, this is a really cool tool and I'd encourage any mathematically-minded person to give it a spin. The only sad thing is that I doubt I'll ever have the opportunity to explore this stuff in my day job unless/until I go back to school :-(.

Shortcomings of Coq specifically and the whole concept of correctness proofs on programs generally have been moved to a future blog post that may never appear depending on how ambitious I'm feeling this week. Rest assured that I'm aware of (some of) them, I just hit my self-imposed length limit.

[0] the reason being that I could only prove correct the formal underpinnings of the resolver; in practice, a lot of the bugs are in the interface to apt, or in apt itself, and I can hardly prove that code correct.