Interactive Theorem Proving and Program Development: Coq'art: The Calculus of Inductive Constructions

Great book! If you like to start with Interactive Theorem Proving

This is the most authoritative text on Coq and Gallina that I am aware of. Somewhat hard to read though.

Coq is a semi automated, interactive theorem prover (colloquially a proof assistant) that works with both math and programming expressions. It's coded in OCaml, it's a generally functional paradigm, and its typing discipline is static and strong. Typing in developing new programming languages is about ontology and taxonomy (how classes, objects, organization, methods, classifications and much more are set up and separated), NOT typing on a keyboard. Typing is the way programs check for consistency, which is a kind of error detection and/or avoidance, and thus VERY relevant to Coq.Speaking of typing, you MUST understand typing to use this book. Any book on developing new programming languages (and some on DSLs) will cover typing if written after the 90's (/during oop season), but if you have cash to burn, Ben Pierce is the go to guy on that: Types and Programming Languages, available used for about $30+ US on Amazon.Both the 2004 and 2005 hardcover and paperback of this book are the same, so shop for the best price. These books cover several releases back, and the stable releases from 2013 and up are not backward compatible. The software is freely available at coq dot inria dot fr, and you will need it to use this book. Ssreflect, a significant new set of tools for Coq, also is freely available and is not covered except on the website. (You CANNOT get this book on a website, or free, the documentation does NOT include this book's pedagogy).This book is a MUST as a great general intro to how, where and why to use Coq. All the documentation information in this book, as well as a tutorial, are available on the inria website, but are not organized for learning or for beginners, autodidacts or self study as this fine text is. BUT the weaknesses of the book being dated are made up for on the website, which DOES have an 8.4 and above tutorial that you will understand easily after studying this book. Note that this is still the ONLY well written, BEGINNERS intro to Coq!Coq USED to be (when this book was written) a research and development tool, and basically non-commercial. However, since that time, Coq has proven a number of practical theorems and has validated two new optimizing compilers (CompCert for C and one for Java). Because of this, Coq has suddenly become the "go to" solver/ proof engine for new languages that have to be validated and bulletproof at launch. I write domain specific languages for robotics, and although I don't achieve bulletproof in my compiles (which are at the VHDL/ circuit level), Coq is a wonderful "debugging" tool as well. It doesn't provide the level of code generation of Isabelle, but other than that is clearly the top proof assistant available.Experience in OCaml is a plus, and Haskell is "almost" a necessity if you are developing a compiler to interact with the OCaml. Haskell's "lazy" access system also allows you to deluge the compiler with test junk that's only used if needed, so you don't have to worry about blowing out your memory when Coq decides to gallop. This book is for mature developers of new languages, and programmers that are interested in checking their code in a semi automated fashion, so obviously you need to know how to code-- well-- to use this book and these tools.Library Picks reviews only for the benefit of Amazon shoppers and has nothing to do with Amazon, the authors, manufacturers or publishers of the items we review. We always buy the items we review for the sake of objectivity, and although we search for gems, are not shy about trashing an item if it's a waste of time or money for Amazon shoppers. If the reviewer identifies herself, her job or her field, it is only as a point of reference to help you gauge the background and any biases.