Lambda the Ultimate

"Relatively practical" seems be about the right description. I've been experimenting with Coq for a little while now and it feels like proving things (even simple things) is a constant battle. Benton's publications page, mentions his thoughts on the process in Machine Obstructed Proof (Abstract).

Tactics feel especially uncomfortable. Reading a proof, its difficult to figure out what the invocation of a tactic is supposed to accomplish. It takes a lot of experience to know how a complex tactic will interact with a context/term. The tactic language, Ltac, itself is interesting. Its untyped and uses non-linear pattern matching and backtracking extensively. David Delahaye's A Proof Dedicated Meta-Language explains some of the engineering trade-offs in the design of Ltac.

(This is mostly in response to the Machine Obstructed Proof abstract.)

I've said before that it seems that the CS folk are getting much more out of CH than the logicians. However, one area that computer scientists seem to have a much better grasp on than mathematicians (for proofs and proving) is modularity and (the very subjective form of) "expressiveness" and "control". Feeding back programming techniques into mathematics via Curry-Howard seems like a way to "repay the debt". Of course, there are some issues: First, the proof assistants are almost certainly already far on the CS-side of the fence. Second, while modularity techniques allow programmers to build large programs, most mathematicians are not interested in large proofs as the main reason to prove something is for understanding, a proof too large to grasp is usually not very interesting.

These are good points—I've begun to go through the Coq tutorial at long last, and I can't help but notice that even the tutorial assumes that you know what tactics, e.g. elimination, to apply in what situations, e.g. conjunction. Well, it's been a looooooooong time since I've studied logic, so I don't remember that stuff. auto, tauto, and trivial are pretty cool, however, and I'm sufficiently intrigued by the approach, the availability of Benton and Leroy's efforts, and the general maturity of Coq to have shelled out the bucks for Coq'Art. Hopefully this will help shed some light on the issues. And thanks for the pointers!

I've now read the paper, and I have to say I found it disappointing: I think I can summarize it effectively as "Creating machine-checked proofs requires a huge up-front investment, but once you've done it a few times, oh my goodness is it worth it in the end." Well, as I've written before, learning to program effectively in [paradigm X] takes years of up-front effort, but oh my goodness is it worth it in the end. I can't help but wonder why people are willing to invest years in learning C++/Java/C#/.NET but not months in learning a tool like Coq or MetaPRL or Twelf or Maude or OBJ3.

I can't help but wonder why people are willing to invest years in learning C++/Java/C#/.NET but not months in learning a tool like Coq or MetaPRL or Twelf or Maude or OBJ3.

Because the former tools pay the bills and are widely used and documented. The payoff is clear. It's not so clear whether tools like Coq are worth it to the average programmer.

I found the "paper" (it is just 1 page, right?) very valuable. It was a refreshingly honest description of his experience, both the good and the bad. This is exactly the kind of material somebody wandering in to the field needs to avoid being blindsided. I wish I had read something similar before my adventures with Haskell or Isabelle.

My point was that the paper did precisely nothing to help delineate contexts in which the investment in learning a proof assistant pays off and contexts in which it doesn't. To me, all the paper said was "learning Coq made my brain hurt, but in the end it's generally useful, so the investment was worth it." Now, that's almost certainly an overgeneralization: given that the application domain is programming language design, a better summary might be "Learning Coq made my brain hurt, but in the end it's extremely useful for programming language design, and hence worth it." But as you can see, it didn't take anywhere near even a page to say that, so I'm still trying to figure out what the point was.

Update: I also am of the opinion that learning a good (especially well-documented, like Coq or Maude) theorem-prover is a lot like learning Lisp: learning it will make you a better programmer, no matter what languages/frameworks you end up using in practice.

But as you can see, it didn't take anywhere near even a page to say that, so I'm still trying to figure out what the point was.

His point was to describe in detail his experience. I'm glad he shared -- I found it valuable. I will leave it at that.

I didn't mean to imply that no one should find value in it—actually, given his depth of experience, lots of folks will likely find his frustration informative—only that I personally didn't learn anything from it, possibly with the generalization that I don't think anyone who's spent much time around type theory or typed programming language design will benefit from it—that is, someone, e.g. who's at least worked through TAPL. Obviously, that's an opinion that not everyone will share. I suppose I also am of the opinion that someone trying to design a statically typed programming language today without benefit of proof assistant is probably working too hard, but that's admittedly likely to be controversial.

I also am of the opinion that learning a good (especially well-documented, like Coq or Maude) theorem-prover is a lot like learning Lisp: learning it will make you a better programmer, no matter what languages/frameworks you end up using in practice.

I don't think many would doubt that you'd learn something from the experience, but if we are wondering about the lack of popularity, one could also ask about the opportunity costs involved. Instead of learning something like Coq, maybe a person could tackle things like QuickCheck and Alloy (or similar, ???) and capture 80% of the value for 20% of the cost? (This coming from someone who is currently working through both Coq'Art and the ACL2 book.)

First, let me strongly state my opinion that this is the right question to ask: what is the economics of choosing tools and methodologies in pursuit of the design of anything?

I don't yet know how to resolve the question of using Alloy for programming language design, but IMHO it's a question that needs resolving, because one of the great benefits of Alloy is the extent to which it lends itself to incremental specification. So far, this seems to be in stark contrast to the various proof assistants, which seem to be "all or nothing" propositions (but note that I have not yet completely worked through even a tutorial for any given proof assistant, let alone worked through a comprehensive text, so I may be all wet on this). On the other hand, even with the Small Scope Hypothesis accepted, I'm not sure that I would want to attempt to design the successor to Java 5, C# 3.0, C++, O'Caml 3.09, Haskell 98, GHC 6.4.x... with a "theorem refuter" that might somehow fail to find a counterexample, vs. a proof assistant that will help me construct an iron-clad (modulo limitations of the logic in question) proof of the properties I expect my language to have.

Still, if the goal isn't to create an industrial-strength language in the sense just mentioned, but rather to learn how to apply proof-theoretic tools to the process of language design, a "theorem refuter" may serve perfectly well, and I'd love to see someone tackle such a process with Alloy.