Mercurial > cpdt > repo

comparison src/Intro.v @ 399:5986e9fd40b5

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Start figuring out which coqdoc changes will be needed to produce a pretty final version
author Adam Chlipala <adam@chlipala.net>
date Fri, 08 Jun 2012 11:25:11 -0400
parents 05efde66559d
children eda5f4eb21b4
comparison
equal deleted inserted replaced
398:05efde66559d 399:5986e9fd40b5
20 20
21 Around the beginning of the 21st century, the pace of progress in practical applications of interactive theorem proving accelerated significantly. Several well-known formal developments have been carried out in Coq, the system that this book deals with. In the realm of pure mathematics, Georges Gonthier built a machine-checked proof of the four color theorem%~\cite{4C}%, a mathematical problem first posed more than a hundred years before, where the only previous proofs had required trusting ad-hoc software to do brute-force checking of key facts. In the realm of program verification, Xavier Leroy led the CompCert project to produce a verified C compiler back-end%~\cite{CompCert}% robust enough to use with real embedded software. 21 Around the beginning of the 21st century, the pace of progress in practical applications of interactive theorem proving accelerated significantly. Several well-known formal developments have been carried out in Coq, the system that this book deals with. In the realm of pure mathematics, Georges Gonthier built a machine-checked proof of the four color theorem%~\cite{4C}%, a mathematical problem first posed more than a hundred years before, where the only previous proofs had required trusting ad-hoc software to do brute-force checking of key facts. In the realm of program verification, Xavier Leroy led the CompCert project to produce a verified C compiler back-end%~\cite{CompCert}% robust enough to use with real embedded software.
22 22
23 Many other recent projects have attracted attention by proving important theorems using computer proof assistant software. For instance, the L4.verified project%~\cite{seL4}% has given a mechanized proof of correctness for a realistic microkernel, using the Isabelle/HOL proof assistant%~\cite{Isabelle/HOL}\index{Isabelle/HOL}%. The amount of ongoing work in the area is so large that I cannot hope to list all the recent successes, so from this point I will assume that the reader is convinced both that we ought to want machine-checked proofs and that they seem to be feasible to produce. (To readers not yet convinced, I suggest a Web search for %``%#"#machine-checked proof#"#%''%!) 23 Many other recent projects have attracted attention by proving important theorems using computer proof assistant software. For instance, the L4.verified project%~\cite{seL4}% has given a mechanized proof of correctness for a realistic microkernel, using the Isabelle/HOL proof assistant%~\cite{Isabelle/HOL}\index{Isabelle/HOL}%. The amount of ongoing work in the area is so large that I cannot hope to list all the recent successes, so from this point I will assume that the reader is convinced both that we ought to want machine-checked proofs and that they seem to be feasible to produce. (To readers not yet convinced, I suggest a Web search for %``%#"#machine-checked proof#"#%''%!)
24 24
25 The idea of %\index{certified program}%_certified program_ features prominently in this book's title. Here the word %``%#"#certified#"#%''% does _not_ refer to governmental rules for how the reliability of engineered systems may be demonstrated to sufficiently high standards. Rather, this concept of certification, a standard one in the programming languages and formal methods communities, has to do with the idea of a _certificate_, or formal mathematical artifact proving that a program meets its specification. Government certification procedures rarely provide strong mathematical guarantees, while certified programming provides guarantees about as strong as anything we could hope for. We trust the definition of a foundational mathematical logic, we trust an implementation of the logic, and we trust that we have encoded our informal intent properly in formal specifications, but little else is left open as an opportunity to certify incorrect software. For programs like compilers that run in batch mode, the notion of a %\index{certifying program}%_certifying_ program is also common, where each run of the program outputs both an answer and a proof that it is correct. Certified software can be considered to subsume certifying software, and this book focuses on the certified case, while also introducing principles and techniques of general interest for stating and proving theorems in Coq. 25 The idea of %\index{certified program}% _certified program_ features prominently in this book's title. Here the word %``%#"#certified#"#%''% does _not_ refer to governmental rules for how the reliability of engineered systems may be demonstrated to sufficiently high standards. Rather, this concept of certification, a standard one in the programming languages and formal methods communities, has to do with the idea of a _certificate_, or formal mathematical artifact proving that a program meets its specification. Government certification procedures rarely provide strong mathematical guarantees, while certified programming provides guarantees about as strong as anything we could hope for. We trust the definition of a foundational mathematical logic, we trust an implementation of the logic, and we trust that we have encoded our informal intent properly in formal specifications, but little else is left open as an opportunity to certify incorrect software. For programs like compilers that run in batch mode, the notion of a %\index{certifying program}% _certifying_ program is also common, where each run of the program outputs both an answer and a proof that it is correct. Certified software can be considered to subsume certifying software, and this book focuses on the certified case, while also introducing principles and techniques of general interest for stating and proving theorems in Coq.
26 26
27 %\medskip% 27 %\medskip%
28 28
29 There are a good number of (though definitely not %``%#"#many#"#%''%) tools that are in wide use today for building machine-checked mathematical proofs and machine-certified programs. The following is my attempt at an exhaustive list of interactive %``%#"#proof assistants#"#%''% satisfying a few criteria. First, the authors of each tool must intend for it to be put to use for software-related applications. Second, there must have been enough engineering effort put into the tool that someone not doing research on the tool itself would feel his time was well spent using it. A third criterion is more of an empirical validation of the second: the tool must have a significant user community outside of its own development team. 29 There are a good number of (though definitely not %``%#"#many#"#%''%) tools that are in wide use today for building machine-checked mathematical proofs and machine-certified programs. The following is my attempt at an exhaustive list of interactive %``%#"#proof assistants#"#%''% satisfying a few criteria. First, the authors of each tool must intend for it to be put to use for software-related applications. Second, there must have been enough engineering effort put into the tool that someone not doing research on the tool itself would feel his time was well spent using it. A third criterion is more of an empirical validation of the second: the tool must have a significant user community outside of its own development team.
30 30