Mercurial > cpdt > repo

comparison src/Intro.v @ 393:d40b05266306

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Define 'certified program'
author Adam Chlipala <adam@chlipala.net>
date Sun, 22 Apr 2012 15:38:11 -0400
parents 76e1dfcb86eb
children d62ed7381a0b
comparison
equal deleted inserted replaced
392:4b1242b277b2 393:d40b05266306
19 Research into mechanized theorem proving began around the 1970's, and some of the earliest practical work involved Nqthm%~\cite{Nqthm}\index{Nqthm}%, the %``%#"#Boyer-Moore Theorem Prover,#"#%''% which was used to prove such theorems as correctness of a complete hardware and software stack%~\cite{Piton}%. ACL2%~\cite{CAR}\index{ACL2}%, Nqthm's successor, has seen significant industry adoption, for instance, by AMD to verify correctness of floating-point division units%~\cite{AMD}%. 19 Research into mechanized theorem proving began around the 1970's, and some of the earliest practical work involved Nqthm%~\cite{Nqthm}\index{Nqthm}%, the %``%#"#Boyer-Moore Theorem Prover,#"#%''% which was used to prove such theorems as correctness of a complete hardware and software stack%~\cite{Piton}%. ACL2%~\cite{CAR}\index{ACL2}%, Nqthm's successor, has seen significant industry adoption, for instance, by AMD to verify correctness of floating-point division units%~\cite{AMD}%.
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
25 The idea of %\index{certified program}\emph{%#<i>#certified program#</i>#%}% features prominently in this book's title. Here the word %``%#"#certified#"#%''% does %\emph{%#<i>#not#</i>#%}% 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 %\emph{%#<i>#certificate#</i>#%}%, 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}\emph{%#<i>#certifying#</i>#%}% 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
27 %\medskip%
24 28
25 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.
26 30
27 % 31 %
28 \medskip 32 \medskip