Mercurial > cpdt > repo

comparison src/Intro.v @ 244:0400fa005d5a

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
New release
author Adam Chlipala <adamc@hcoop.net>
date Wed, 09 Dec 2009 14:12:33 -0500
parents 52b9e43be069
children de53c8bcfa8d
comparison
equal deleted inserted replaced
243:b2c72c77ad47 244:0400fa005d5a
47 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. 47 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.
48 48
49 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. This 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. 49 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. This 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.
50 50
51 % 51 %
52 \medskip
53
52 \begin{tabular}{rl} 54 \begin{tabular}{rl}
53 \textbf{ACL2} & \url{http://www.cs.utexas.edu/users/moore/acl2/} \\ 55 \textbf{ACL2} & \url{http://www.cs.utexas.edu/users/moore/acl2/} \\
54 \textbf{Coq} & \url{http://coq.inria.fr/} \\ 56 \textbf{Coq} & \url{http://coq.inria.fr/} \\
55 \textbf{Isabelle/HOL} & \url{http://isabelle.in.tum.de/} \\ 57 \textbf{Isabelle/HOL} & \url{http://isabelle.in.tum.de/} \\
56 \textbf{PVS} & \url{http://pvs.csl.sri.com/} \\ 58 \textbf{PVS} & \url{http://pvs.csl.sri.com/} \\
57 \textbf{Twelf} & \url{http://www.twelf.org/} \\ 59 \textbf{Twelf} & \url{http://www.twelf.org/} \\
58 \end{tabular} 60 \end{tabular}
61
62 \medskip
59 % 63 %
60 # 64 #
61 <table align="center"> 65 <table align="center">
62 <tr><td align="right"><b>ACL2</b></td> <td><a href="http://www.cs.utexas.edu/users/moore/acl2/">http://www.cs.utexas.edu/users/moore/acl2/</a></td></tr> 66 <tr><td align="right"><b>ACL2</b></td> <td><a href="http://www.cs.utexas.edu/users/moore/acl2/">http://www.cs.utexas.edu/users/moore/acl2/</a></td></tr>
63 <tr><td align="right"><b>Coq</b></td> <td><a href="http://coq.inria.fr/">http://coq.inria.fr/</a></td></tr> 67 <tr><td align="right"><b>Coq</b></td> <td><a href="http://coq.inria.fr/">http://coq.inria.fr/</a></td></tr>