## Mercurial > cpdt > repo

### comparison src/Conclusion.v @ 510:fd6ec9b2dccb

Find changesets by keywords (author, files, the commit message), revision
number or hash, or revset expression.

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 |

comparison

equal
deleted
inserted
replaced

509:21079e42b773 | 510:fd6ec9b2dccb |
---|---|

7 * http://creativecommons.org/licenses/by-nc-nd/3.0/ | 7 * http://creativecommons.org/licenses/by-nc-nd/3.0/ |

8 *) | 8 *) |

9 | 9 |

10 (** %\addcontentsline{toc}{chapter}{Conclusion}\chapter*{Conclusion}% *) | 10 (** %\addcontentsline{toc}{chapter}{Conclusion}\chapter*{Conclusion}% *) |

11 | 11 |

12 (** 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. | 12 (** 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. |

13 | 13 |

14 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. | 14 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. |

15 | 15 |

16 As Coq has so many moving parts to catalogue mentally, I have not attempted to describe most of them here; nor have I attempted to give exhaustive descriptions of the few I devote space to. To those readers who have made it this far through the book, my advice is: read through the Coq manual, front to back, at some level of detail. Get a sense for which bits of functionality are available. Dig more into those categories that sound relevant to the developments you want to build, and keep the rest in mind in case they come in handy later. | 16 As Coq has so many moving parts to catalogue mentally, I have not attempted to describe most of them here; nor have I attempted to give exhaustive descriptions of the few I devote space to. To those readers who have made it this far through the book, my advice is: read through the Coq manual, front to back, at some level of detail. Get a sense for which bits of functionality are available. Dig more into those categories that sound relevant to the developments you want to build, and keep the rest in mind in case they come in handy later. |

17 | 17 |