Mercurial > cpdt > repo
diff src/Conclusion.v @ 510:fd6ec9b2dccb
Finished last pass through the book before beginning the MIT Press editorial process
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Wed, 13 Feb 2013 10:22:18 -0500 |
| parents | 5986e9fd40b5 |
| children |
line wrap: on
line diff
--- a/src/Conclusion.v Tue Feb 12 11:14:52 2013 -0500 +++ b/src/Conclusion.v Wed Feb 13 10:22:18 2013 -0500 @@ -9,7 +9,7 @@ (** %\addcontentsline{toc}{chapter}{Conclusion}\chapter*{Conclusion}% *) -(** I have designed this book to present the key ideas needed to get started with productive use of Coq. Many people have learned to use Coq through a variety of resources, yet there is a distinct lack of agreement on structuring principles and techniques for easing the evolution of Coq developments over time. Here I have emphasized two unusual techniques: programming with dependent types, and proving with scripted proof automation. I have also tried to present other material following my own take on how to keep Coq code beautiful and scalable. +(** I have designed this book to present the key ideas needed to get started with productive use of Coq. Many people have learned to use Coq through a variety of resources, yet there is a distinct lack of agreement on structuring principles and techniques for easing the evolution of Coq developments over time. Here I have emphasized two unusual techniques: programming with dependent types and proving with scripted proof automation. I have also tried to present other material following my own take on how to keep Coq code beautiful and scalable. Part of the attraction of Coq and similar tools is that their logical foundations are small. A few pages of %\LaTeX{}%#LaTeX# code suffice to define CIC, Coq's logic, yet there do not seem to be any practical limits on which mathematical concepts may be encoded on top of this modest base. At the same time, the _pragmatic_ foundation of Coq is vast, encompassing tactics, libraries, and design patterns for programs, theorem statements, and proof scripts. I hope the preceding chapters have given a sense of just how much there is to learn before it is possible to drive Coq with the same ease with which many readers write informal proofs! The pay-off of this learning process is that many proofs, especially those with many details to check, become much easier to write than they are on paper. Further, the truth of such theorems may be established with much greater confidence, even without reading proof details.