Mercurial > cpdt > repo

comparison book/src/Intro.v @ 5:aa32e9f63da0

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
More of Intro
author Adam Chlipala <adamc@hcoop.net>
date Fri, 29 Aug 2008 17:20:57 -0400
parents f913d32a49e4
children 6cc7a8fd4a8c
comparison
equal deleted inserted replaced
4:f913d32a49e4 5:aa32e9f63da0
105 (** 105 (**
106 A surprising wealth of benefits follow from choosing a proof language that integrates a rich notion of computation. Coq includes programs and proof terms in the same syntactic class. This makes it easy to write programs that compute proofs. With rich enough dependent types, such programs are %\textit{%#<i>#certified decision procedures#</i>#%}%. In such cases, these certified procedures can be put to good use %\textit{%#<i>#without ever running them#</i>#%}%! Their types guarantee that, if we did bother to run them, we would receive proper "ground" proofs. 106 A surprising wealth of benefits follow from choosing a proof language that integrates a rich notion of computation. Coq includes programs and proof terms in the same syntactic class. This makes it easy to write programs that compute proofs. With rich enough dependent types, such programs are %\textit{%#<i>#certified decision procedures#</i>#%}%. In such cases, these certified procedures can be put to good use %\textit{%#<i>#without ever running them#</i>#%}%! Their types guarantee that, if we did bother to run them, we would receive proper "ground" proofs.
107 107
108 The critical ingredient for this technique, many of whose instances are referred to as %\textit{%#<i>#proof by reflection#</i>#%}%, is a way of inducing non-trivial computation inside of logical propositions during proof checking. Further, most of these instances require dependent types to make it possible to state the appropriate theorems. Of the proof assistants I listed, only Coq really provides this support. 108 The critical ingredient for this technique, many of whose instances are referred to as %\textit{%#<i>#proof by reflection#</i>#%}%, is a way of inducing non-trivial computation inside of logical propositions during proof checking. Further, most of these instances require dependent types to make it possible to state the appropriate theorems. Of the proof assistants I listed, only Coq really provides this support.
109 *) 109 *)
110
111
112 (** * Engineering with a Proof Assistant *)
113
114 (**
115 In comparisons with its competitors, Coq is often derided for promoting unreadable proofs. It is very easy to write proof scripts that manipulate proof goals imperatively, with no structure to aid readers. Such developments are nightmares to maintain, and they certainly do not manage to convey "why the theorem is true" to anyone but the original author. One additional (and not insignificant) purpose of this book is to show why it is unfair and unproductive to dismiss Coq based on the existence of such developments.
116
117 I will go out on a limb and guess that the reader is a dedicated fan of some functional programming language or another, and that he may even have been involved in teaching that language to undergraduates. I want to propose an analogy between two attitudes: coming to a negative conclusion about Coq after reading common Coq developments in the wild, and coming to a negative conclusion about Your Favorite Language after looking at the programs undergraduates write in it in the first week of class. The pragmatics of mechanized proving and program verification have been under serious study for much less time than the pragmatics of programming have been. The computer theorem proving community is still developing the key insights that correspond to those that functional programming texts and instructors impart to their students, to help those students get over that critical hump where using the language stops being more trouble than it is worth. Most of the insights for Coq are barely even disseminated among the experts, let alone set down in a tutorial form. I hope to use this book to go a long way towards remedying that.
118
119 If I do that job well, then this book should be of interest even to people who have participated in classes or tutorials specifically about Coq. The book should even be useful to people who have been using Coq for years but who are mystified when their Coq developments prove impenetrable by colleagues. The crucial angle in this book is that there are "design patterns" for reliably avoiding the really grungy parts of theorem proving, and consistent use of these patterns can get you over the hump to the point where it is worth your while to use Coq to prove your theorems and certify your programs, even if formal verification is not your main concern in a project. We will follow this theme by pursuing two main methods for replacing manual proofs with more understandable artifacts: dependently-typed functions and custom Ltac decision procedures.
120 *)
121
122
123 (** * Prerequisites for This Book *)
124
125 (**
126 I try to keep the required background knowledge to a minimum in this book. I will assume familiarity with the material from usual discrete math and logic courses taken by all undergraduate computer science majors, and I will assume that readers have significant experience programming in one of the ML dialects, in Haskell, or in some other, closely-related language. Experience with only dynamically-typed functional languages might lead to befuddlement in some places, but a reader who has come to grok Scheme deeply will probably be fine.
127
128 A good portion of the book is about how to formalize programming languages, compilers, and proofs about them. I depart significantly from today's most popular methodology for pencil-and-paper formalism among programming languages researchers. There is no need to be familiar with operational semantics, preservation and progress theorems, or any of the material found in courses on programming language semantics but not in basic discrete math and logic courses. I will use operational semantics very sparingly, and there will be no preservation or progress proofs. Instead, I will use a style that seems to work much better in Coq, which can be given the fancy-sounding name %\textit{%#<i>#foundational type-theoretic semantics#</i>#%}% or the more populist name %\textit{%#<i>#semantics by definitional compilers#</i>#%}%.
129 *)