Lambda the Ultimate

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

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

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.

Even for those of us who have some experience with other provers, the Coq documents qualify as opaque. A student who is fairly experienced mentioned earlier today that he was finding it much easier to learn Coq by studying the theorem library than by reading the documentation (which is saying something). On the other hand, he also said that he really liked what he was seeing, and that thinking about how to express one of his verification challenges to Coq may have given him a breakthrough on pushing the same problem through ACL2.

Our experience to date is that the challenge in verification more often lies in prover management than in the proof itself. Sadly, this seems to be independent of any particular prover.:-)

I'm certainly guilty of not having clarified any part of Coq's documentation while being a major contributor to the tool for 3 years now, but time spent on documentation is spent not fixing bugs or doing research so there's a big tension there :). However, there are much more accessible resources out there, including the Coq'Art book and some tutorials. I'd like to mention that Adam is currently writting another tutorial oriented on practical aspects of the tool. To "Get things done", as you mention, you need to be able to manage the proving machinery as easily as possible. This power is given in Coq by the turing-complete, mostly-untyped Ltac language that allows to engineer the process of proving up to the point of building domain-specific libraries of tactics that let you solve your goals with one-liners. This kind of user-driven automation seems like a good step towards having a methodology of writing clear and robust proofs in these systems.

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.

When writing a tutorial, you are torn between conflicting objectives. One of the objectives is to demonstrate the usefulness of a theorem prover for the "normal programmer". For this objective, you don't really need to use a theorem prover specifically, they are all good enough to provide an introduction. Actually, I am afraid that a more powerful tool might even be less good for this purpose, because you need to teach how to harness the power. The second objective is to advocate a specific tool in particular, and this objective can be very detrimental for the usefulness of your tutorial: you are dragged into studying examples that illustrate the obscure ways in which your pet tool is better than the others...

When working specifically on Coq, the risk is to delve too much into dependent types, the Curry-Howard isomorphism, and inductive types, although these could probably be avoided (or minimized, using dependent types only to describe polymorphic functions, using inductive types only to produce the same non-dependent types as those used in conventional functional programming languages, and hiding the Curry-Howard isomorphism behind the "Lemma-tactics-Qed" mechanics for proof building).

For introductory material on Theorem proving in general, I would like to mention the book edited by F. Wiedijk, The seventeen theorem provers of the world, this is not about program verification (so maybe not of interest for the normal programmer), but it gives a comparative study of proving the same fact in different settings. It is interesting that not all participants prove the same thing!

This is all good advice. But I feel compelled to respond with a (hopefully humorous) word of caution for the benefit of newcomers to provers.

It is very easy to use a prover for a few days or weeks and decide that it is the right tool for you. This is particularly seductive when the prover is aggressively automated (as in ACL2 or TWELF). You develop a strong sense that you are making good progress, and you begin to wonder why people keep saying that this prover stuff is so hard. It's all rather seductive.

And then you decide to try something more substantial, and all of a sudden you discover that all of that automation is gleefully automating its way down dead ends using every theorem you have (especially including the irrelevant ones) and every theorem that it can combinatorically derive from those. And it turns out that after ten layers of onion peeling your problem structure doesn't quite fit the available induction tactics. And there you are, deep in a subgoal generated by a completely irrelevant induction strategy, looking at a goal that looks suspiciously like a irreducible rewrite of something you think you have already solved, only improved with unreadable variable names that you brain can almost pattern match. At this point it occurs to you that your shiny new prover has suddenly developed this ugly tarnished look. Welcome to what my lab finally calls prover hell. Every prover has its challenges. You've hit yours and the prover honeymoon is over.

If all of this is standing between you and completing your PhD, this is the point where switching to an MBA really starts to look like an easy way out (and actually, it probably is an easier way out).

My advice is simply: don't panic at this point. If you get deep enough into the bear trap to find that your leg is well and truly caught, you have learned quite a lot. It may turn out (in fact, it's likely) that switching to a different (and less automated) prover will be the right way out for you, but by this point you probably won't need the automation anymore, and you'll probably find that this completely opaque Coq thing (or Isabelle, or PVS...) almost makes sense to you now.

Congratulations. You're now (with good-humored apologies to Paul) a theory weenie. :-)

At this point, feel free to call someone in my lab. We can help you find your inner systems hacker again. We have this simple twelve step program...

When you're right, you're right!

In Coq's defense (not that I really think it needs it), it's not all that automated. I'd say that it has some tools that you can try on your subgoals. Some of those tools are very small in scope, and some are not. Some change your subgoals when they fail, and some don't. But failing all else, you can always fall back on the extremely primitive ones.

This is admittedly in contrast to tools like Twelf, where your choices are to write the proof term by hand, or to write some Standard ML to automate some decision procedure and link it into your Twelf binary. But it's also in contrast to fully automated model checkers, SAT solvers, Prolog, and the like.

Finally, shap is, of course, correct in saying both that you can end up in a maze of twisty little passages, all isomorphic up to alpha conversion; and that once you pile-drive your way through that wall, you're a theory weenie like me! Actually, I'm more of a wanna-be still: I emphatically do not claim to be a Coq expert. Rather, Coq expertise is something that I aspire to, and occasionally talk about online when it seems like there's an opportunity to share what I've learned so far, or to refer to the excellent work that others have done.

For those who take Shap's advice to follow the MBA path, let me highly recommend How to Write a Financial Contract. :-)

And here I thought that MBAs are becoming less attractive...

Given a choice between sitting through an MBA program and slogging through an obnoxious proof, which one would you prefer?

I've gone through the first lecture, and HW0 (using coqide to follow along). But I don't follow the proof in HW0.... he says "I'm not expecting you to understand what this code means, but rather just to get a feel for the Proof General interaction process.", but then later says "You can probably see that the formula in this case is obviously true". But I don't see how the cons subgoal is produced, even though it is "obvious" and "trivial".

When he says that, he's speaking about the current goal (which is "append ls2 ls3 = append ls2 ls3") which you probably agree is obvious ?

The induction process by itself isn't that simple (there are after all something like 6 tactics that do "induction" in Coq, and you can write custom induction scheme too...), though you should still be able to recognize a structural induction like you would do by hand (proving the property if ls1 is "nil", if ls1 is "cons x ls1' " supposing you know that it is true for ls1' (substructure of ls1) and proving it for ls1 under this hypothesis).

Don't worry too much if you don't understand how Coq derived the induction yet, that's a pretty complex subject over which you'll come back.

Thanks for your reply - I thought it was talking about both subgoals (and I see now it collapses the first subgoal when you progress). Yes, the first subgoal is obvious, but the second subgoal confuses me. I think I understand induction, but not "structural induction". I recognize the base case of ls1 = nil, but not the case of ls1 = cons x ls1' EDIT now I understand; I've added my step-by-step explanation. Here's a direct link to HW0

The first subgoal, with ls1 = nil, is:

   append (append ls1 ls2) ls3 = append ls1 (append ls2 ls3)
   append (append nil ls2) ls3 = append nil (append ls2 ls3)
Using the rule: append (nil b) => b
   =>  append ls2 ls3 = append ls2 ls3

The second subgoal, with ls1 = cons x ls1' is:

   append (append ls1           ls2) ls3 = append ls1           (append ls2 ls3)
   append (append (cons x ls1') ls2) ls3 = append (cons x ls1') (append ls2 ls3)
Using the rule 3 times: append ((cons x a') b) => cons x (append a' b)
   =>  append (cons x (append ls1' ls2)) ls3 = append (cons x ls1') (append ls2 ls3)
   =>  cons x (append (append ls1' ls2) ls3 = append (cons x ls1') (append ls2 ls3)
   =>  cons x (append (append ls1' ls2) ls3 = cons x (append ls1' (append ls2 ls3))

I just had to apply the rule. The induction is that for any ls1, the "head" can be moved out one by one, until nil is left. This is the base case, which is known to be equal.

Thanks for taking the time to reply with your suggestion - it helped me to see more.