Home

Certified Programming With Dependent Types Goes Beta

Certified Programming With Dependent Types

From the introduction:

We would all like to have programs check that our programs are correct. Due in no small part to some bold but unfulfilled promises in the history of computer science, today most people who write software, practitioners and academics alike, assume that the costs of formal program verification outweigh the benefits. The purpose of this book is to convince you that the technology of program verification is mature enough today that it makes sense to use it in a support role in many kinds of research projects in computer science. Beyond the convincing, I also want to provide a handbook on practical engineering of certified programs with the Coq proof assistant.

This is the best Coq tutorial that I know of, partially for being comprehensive, and partially for taking a very different tack than most with Adam's emphasis on proof automation using Coq's Ltac tactic language. It provides an invaluable education toward understanding what's going on either in LambdaTamer or Ynot, both of which are important projects in their own rights.

Please note that Adam is explicitly requesting feedback on this work.

By Paul Snively at 2010-01-09 16:56 | Functional | Lambda Calculus | Logic/Declarative | Misc Books | Semantics | Teaching & Learning | Type Theory | other blogs | 10873 reads

Comment viewing options

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

Pierce's Software Foundations course

Andrew Chipala's book looks great. Another good introduction to Coq that comes from the PL side of things is Benjamin Pierce's Software Foundations course. I heard about it when I watched his keynote address at ICFP 2009. He talks about his teaching experiences, which are generally positive.

The course isn't specifically intended for self study, but the materials are well written and at least Coq always gives me a clear answer about whether or not I've passed an exercise! (I think what Pierce says about the "video game" principle is true. There's something addictive about getting a proof accepted.)

By Rich Dougherty at Sat, 2010-01-09 18:25 | login or register to post comments

Thanks

This is definitely great news. As a practitioner, I only have so much time to evaluate new ideas, and I tend to drift away from ideas where I can't use a textbook to explain the cutting-edge to me. This usually means I'm about 5 years behind the state-of-the-art, but that isn't that bad.

By Z-Bo at Sat, 2010-01-09 18:30 | login or register to post comments

Possible instability in coq?

I have to admit that I'm kind of a dilettante when it comes to proofs. I lack academic credentials. I'm a math/computer geek and I just got it in my head one day that I wanted to do computer-verified proofs. So take this report with an appropriately sized grain of salt.

To make a long story short, I just can't shake the impression that coq isn't stable for large proof scripts. I would have a great big Proof General session open and the system would stop working properly. I would have it reload the file and it would have an error in an earlier part of the file. I had to kill the attached coq process to make things work again.

I also looked over the Coq Proof of the Four Color Theorem. Part of this proof involves exhaustively processing 633 cases. These cases are partitioned into subranges in many files (job001to106.v, job107to164.v, etc). I vaguely remember reading a comment that the work was partitioned because coq was unstable for larger proofs, but I can't seem to find that comment today.

These issues made me fall out of love with coq. I can believe that it sits on a good theoretical foundation, but if the implementation has stability issues, can it be trusted? Again, please take this report with a large grain of salt because I'm just "sharing my feelings", not proving anything.

By novadenizen at Tue, 2010-01-12 17:15 | login or register to post comments

Your concerns are well-aware to those who matter

See Greg Morrisett's and Xavier LeRoy's articles in the Communications of the ACM:
Technical perspective: A compiler's story (this link requires ACM Portals account)
Formal verification of a realistic compiler (Free)

See also Andrew Appel's essay Foundational High-Level Static Analysis (free).

Also, techniques such as separation logic are also only recently achieving scales of being able to go beyond 1M+ lines of code. A lot of this stuff has been funded in part by very long term research initiatives by Microsoft in the area of static analysis.

By Z-Bo at Tue, 2010-01-12 18:01 | login or register to post comments

Good Question

One reason I keep coming back to Coq is that, despite the fact that it can, and does, have bugs, those bugs don't appear to ever pop up in the critical part, which is the proof checker. It's kind of a nice confirmation of the de Bruijn principle: the proof assistant can have bugs, you can write Ltac tactics that have bugs or diverge, etc. But as long as the proof checker is small and simple enough to be audited by hand, all of that is fine.

By Paul Snively at Sat, 2010-01-16 00:10 | login or register to post comments