Machine Obstructed Proof

From ICFP '06, the 1st informal Workshop on Mechanizing Metatheory comes Nick Benton's "Machine Obstructed Proof: How many months can it take to verify 30 assembly instructions?". It is a one page paper, but seems deserving of some notice.

Nick Benton offers a critique of Coq from the standpoint of an inexperienced user, although I am not sure I would really categorize Benton as "inexperienced". Some interesting quotes:

  • "...I have rarely felt as stupid and frustrated as I did during my first few weeks using Coq."
  • "Tactical theorem proving is like an extreme form of aspect-oriented programming. This is not A Good Thing...."
  • "Just having intermediate stages of the work in a computerized form...proved a major benefit."
  • "Automated proving is not just a slightly more fussy version of paper proving and it really like programming."
  • "...but the payoff really came the second time I used Coq: I was able to prove some elementary but delicate just a day or so."

[On edit: moved to a story from a forum post. Sorry. - TM]

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

This was discussed here

This was discussed here before a couple of times. See here.

It wouldn't hurt to give it more exposure, though...


Just in case there's any doubt, I'd just like to go on the record
(I think LtU counts as the record) as saying that Coq is without
doubt one of the most impressive, useful and downright cool bits of
software I've used in the last 20 years. (Computer scientists are
naturally infinitely more formalist than 99% of mathematicians, but my
residual inner Platonist still gets a faintly illicit thrill from the
fact that computers are allowed to get away with doing this sort of
thing at all.) But that's the point - if it were no good, there'd be
no reason to care how hard it was to learn.

Anyway, for those who are interested, the slides from the talk are
online here. They contain a
few more points than were in the 1-page abstract as well as some
detail about what I was actually *doing* with Coq, which is (I hope)
even more interesting than my ranting about the pain I experienced in
the process.

Surley You Jest

(Computer scientists are naturally infinitely more formalist than 99% of mathematicians,

What? The definitions and theorems in mathematics are quite formal. If I recall correctly, the courses I took in computer science were no more formal or less formal than the mathematics courses I took and now teach.

Sorry I didn't mean to put

Sorry I didn't mean to put the comment where I did.

That's not what I meant

I don't mean formalist in the (informal) sense of being careful. I meant it in the philosophical sense of believing mathematics to be about formal symbol manipulation rather than "real" objects.

You are, of course, quite

You are, of course, quite right about this. Lamport makes this point often, BTW.

Less ignorant than yesterday

I took the time to look up formalist and Ok, I see what you are talking about.

Secondary Reaction

Upon reflection, I think my initial reaction to this paper was too harsh. Maybe it's just due to the summary you wrote here, but I think the paper ultimately strikes the right note: learning interactive theorem proving is unlike any other intellectual endeavor with which I'm familiar, and so the initial efforts have that awful thrown-into-the-pool-before-learning-to-swim feeling. There's no getting around the fact that knowing what tactics to use when in all but the most trivial cases is a matter of intuition, that intuition comes from experience, that experience comes from failure, and that failure comes from trying. But once you develop a sufficient level of intuition, tools like Coq really are unbelievably powerful.

"intuition comes from

"intuition comes from experience, that experience comes from failure, and that failure comes from trying."

Hope you don't mind but I think I'm going to use that phrase yoda style from now on.

Far From Minding...

I'm quite flattered!

You are in good company

Key experience

After thinking about it a bit more myself, I think the point is that interactive theorem proving is not programming, nor is it like creating traditional proofs. The hard-won skills for either are probably useful, but if they are not directly applicable then the learning curve for someone who has done a lot of either is going to be painful, given that they look like they would be so similar.

Are there any tutorials or texts that will reduce the pain? I started the Coq tutorial, but did not seem to be getting any traction and put it aside.

I'm not surprised that your

I'm not surprised that your Coq tutorial didn't attract interest as for a 'normal' programmer like myself, it is quite impossible to learn something with..
I think that a better tutorial would take a very small program and show the corresponding 'proofing' session, then would do the same for more complicated programs.


I think the problem here is that such a tutorial would give the impression that you had to write code, then perform whatever (error-prone!) manual transliteration into Coq's logic would be required, and only then could you prove anything, whereas going the other way—describing what you want, logically, to Coq, and then extracting code from that—is automated once the proof exists.

With respect to the learning question, I find Coq'Art fantastic.

Introductory logic via Coq?

I was actually thinking this weekend that a good exercise might be to work through a standard undergraduate logic text using Coq. The logic text I experienced was significantly more formal than most more advanced work that I have seen, and starting in the basement would avoid the complexities of program verification while building the necessary new intuitions.

An intro to logic based on automated tools would be a good basis for introducing those tools more generally, and would probably make introductory logic classes more interesting. But I'm sure someone has already come to that conclusion and done it, right?

(Coq'Art has been staring at the back of my head throughout this discussion, waiting for me to get some time to devote to it. But the table of contents, at a quick glance, is a bit more intimidating than what I've been thinking about.)


It's true that Coq'Art is probably not a good beginning text, but then, I'd argue that Coq isn't a good beginning tool. Perhaps one of the excellent works from Stanford University's CSLI would be better, e.g. "Language, Proof and Logic."


(Note to self.) Along the same lines (comment-45720):

Q: How many Coq programmers does it take to change a lightbulb?

A: Are you kidding? It takes two post-docs six months just to prove that the bulb and the socket are both threaded in the same direction.