Home » forums » LtU Forum

Course on Interactive Computer Theorem Proving Based on Coq

This looks like an excellent introduction to using Coq, with a focus on programming language design: <http://www.cs.berkeley.edu/~adamc/itp>. People who have been looking for "getting started with Coq" resources should certainly check it out.

By Paul Snively at 2007-04-16 04:06 | LtU Forum | previous forum topic | next forum topic | other blogs | 2973 reads

Comment viewing options

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

Very nice

Indeed, it's very good. Most of the literature around Coq is exceedingly technical, so the down-to-earth approach of the course's slides is quite refreshing.

Some of the topics are even quite advanced, e.g. proof by reflection, of which I previously knew the general idea, but nothing approaching the concrete presentation given in the slides.

So, yes, heartily recommended by me, too.

By Lauri Alanko at Tue, 2007-04-17 18:23 | login or register to post comments

A Few More Observations

First, I should point out that this is from Adam Chlipala, who has been kind enough to post here in response to a previous post on his work on a certified compiler for the lambda calculus.

Second, yes, this is a very accessible, yet extremely fast-paced, course. In my mind, I liken it to "The Little Schemer," which is extremely accessible but nevertheless has the reader deriving the applicative-order Y combinator by its end.

Finally, I neglected to note that there's one final lecture that uses Twelf rather than Coq, so presumably there's some opportunity to compare-and-contrast there.

I'm glad, Lauri, that you found it helpful too. :-)

By Paul Snively at Tue, 2007-04-17 18:34 | login or register to post comments

extremely accessible???

A quite big overstatement!
It flew totally over my head, making me think again that 'theorem proving' is truly not for the normal programmer..

By renox at Wed, 2007-04-18 12:32 | login or register to post comments

It's All Relative :-)

OK, yes, "accessible" lies in the eye of the beholder, and I'm coming to the course materials having put a fair amount of effort into refreshing my logic background. So perhaps some introductory materials to the introductory materials :-) might include Language, Proof, and Logic followed by Hyperproof.

As for theorem provers for "normal programmers," you're right, IMHO: probably not. But I think we'll see more language designs and actual compiler implementations that have been proven correct, to some extent "by construction" (that is, extracted mechanically from their proofs) over time, rather than less, thanks to tools like Coq and efforts such as Co-inductive big-step operational semantics, Compcert, Formal verification of a C-compiler front end, A Certified Type-Preserving Compiler from Lambda Calculus to Assembly Language, Abstracting Allocation: The New new Thing, Verifying Semantic Type Soundness of a Simple Compiler, etc.

Hopefully I'm right, and another consequence of that will be that the industry will have identified a new sweet spot—syntactically not too far from modern C++, Java, or C#, but with a type system more like Scala's or Epigram's etc.—that qualifies as Tim Sweeney's The Next Mainstream Programming Language and provides its users a greater, more useful range of Theorems for Free than currently-popular languages do. But even if that came to pass, the number of folks who could effectively use a Calculus-of-Inductive-Constructions-based theorem prover like Coq effectively would indeed remain quite small.

So the question, in my mind, is: would you like to try to design an important new language or not? If so, beating your head against a theorem prover is quite likely to be a good investment.

By Paul Snively at Wed, 2007-04-18 14:50 | login or register to post comments

More Resources

From <http://programming.reddit.com>, some more excellent Coq resources: <http://programming.reddit.com/info/1isbd/comments>.

Of particular note regarding introductory material is the second entry, "Coq in a Hurry." This is the real introduction to Coq in the strong sense that it assumes no prior experience with Coq, nor even that you know or remember, e.g. what "modus ponens" is. It helpfully provides a little table hinting at which tactics to use given what logical connectives in a (sub)goal—something that should help newcomers who immediately feel at sea in the interactive process in Coq. So a very useful pedagogical flow might be from "Coq in a Hurry" to the Coq Tutorial to Mr. Chlipala's course and/or, if you wish to spend the money, to Coq'Art.

By Paul Snively at Wed, 2007-04-18 17:55 | login or register to post comments

Awesome!

Theorem proving as a whole definitely needs more easily-assimilated introductory material and this hits the nail on the head!

Cheers,
Jon.

By jdh30 at Wed, 2007-04-18 06:59 | login or register to post comments

First Blush

So I've taken the time to actually go through Homework 0 and Homework 1 in this course. Homework 0 is really just a Proof General familiarization exercise, but Homework 1 gets into the basics of the Propositional Calculus and First-Order logic.

It basically took me the better part of today, off and on, with pretty frequent breaks due to other obligations, but also a couple of significant breaks when I got stuck and just needed to pull back for a bit. Which leads me to the following observations:

  1. Proof General is a godsend, and Mr. Chlipala's suggestion to enable electric completion is good advice: this makes it possible to save your work at any point, restart Proof General, position the cursor after the period on the theorem you were working on, press ".", and let Proof General/Coq replay everything up to that point.
  2. The exercises are rather obviously intended to help build your intuition about what tactics apply when, and they're remarkably successful at that. Several times I found myself struggling to use my rusty logic skills, finally getting a proof, only to erase the whole thing and do it over, but more cleanly, which leads to...
  3. Intuition matters, and forming your own set of rules of thumb about how to proceed through a proof is important. For example, at least in these propositional and first-order exercises, I found introducing as many implications as possible, then eliminating as many existentials as possible, then eliminating as many universals as possible to be very successful.
  4. Remember that you can "rewrite <-" to reverse the direction of the equality when rewriting. That'll save you an assert/rewrite/reflexive group.
  5. Don't panic if at a certain point your goal is "False!"
  6. Don't force it. At one point I really did walk away from the computer, occupy my mind in another fashion, and come back an hour or so later and complete the proof.
  7. If your proof looks too long to you, it probably is.
  8. Gauge whether theorem-proving is for you by whether you feel a smile on your face when you not only know that ∃ x:A, ∀ y:A, x = y → e = f e, but have proven it.

It's also kind of cool that the homework checking is automatic: you just compile a signature that includes all of the exercises as axioms, include your solution file, and define a module with the given signature and your included solutions as the implementation. If you get no errors, then your proofs are good. :-)

By Paul Snively at Sun, 2007-04-22 05:50 | login or register to post comments