Lambda the Ultimate

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.

(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 the comment where I did.

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 right about this. Lamport makes this point often, BTW.

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

"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.

I'm quite flattered!

Jim Horning :-)

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

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."