Mercurial > cpdt > repo

comparison src/Intro.v @ 20:c0cbf324ec7d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Finished typed example
author Adam Chlipala <adamc@hcoop.net>
date Wed, 03 Sep 2008 16:14:47 -0400
parents ea400f692b07
children 00366a62bd00
comparison
equal deleted inserted replaced
19:5db67b182ef8 20:c0cbf324ec7d
129 129
130 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. 130 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.
131 *) 131 *)
132 132
133 133
134 (** * Prerequisites for This Book *) 134 (** * Prerequisites *)
135 135
136 (** 136 (**
137 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. 137 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.
138 138
139 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>#%}%. 139 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>#%}%.