Interactive Theorem Proving and Program Development: Coq’Art: The Calculus of Inductive Constructions (Texts in Theoretical Computer Science. An EATCS Series)

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.

Contentwise the Book is great. BUT: The Kindle Edition looks like the book has been scanned and is nearly unreadable. If you don't believe it get the preview. If it would be possible i would claim ma money back. I STRONGLY recommend to get one of the paper-editions.

I tried to learn Coq with no success before I got this book. I'm not in school. I'm just a working professional with strong Haskell skills. I'm learning this on my own. Which makes this material, probably, more difficult for me than for a student or grad student who can work with a teacher and other students as they learn.This book really was the only successful approach I've found for learning Coq on my own. The beginning chapters do a great job at slowly introducing the concepts that underly Coq. The typing rules start out overly simple, just to get you started. Then they revisit the typing rules as new concepts are added. Which, even outside of Coq, is very useful. The explanations at each point are very clear. By the end of chapter 6 I was comfortable with the concepts that underly Coq's type system. The later chapters go over more advanced topics which included program extraction. Program extraction was really the point at which I went "Ah ha!" and started to understand how I could apply Coq to practical applications. After several unsuccessful attempts this really was a great achievement for me. If I knew I would have a good understanding of these concepts for only a ~100$ investment I would have bought this book when it first came out. That would have saved me a lot of unnecessary struggles.The downsides:* The book is slightly out of date. Coq 8.4 (the latest as of the writing of this review) is more capable than the Coq 8.1 (?) the book was written against. There are several instances where the book explicitly says to try something to observe Coq failing. However, Coq 8.4 would rarely fail as the book described. Which is nice in a way but can be confusing. After chapter 5 this occurs less and less.* The book references O'Caml more than Haskell. IMO Haskell is a better suited language for this system. YMMV ;-)* For the most part you can follow along with the book in the coq toplevel. However, sometimes they omit definitions. Which caused me to struggle figuring out what I did wrong in transcribing the book. Only to discover I did nothing wrong and the book was skipping ahead a bit. By chapter 6 I don't recall this being an issue.Note: I would rate this 4 stars but due to the 1 star review due to the poor kindle edition I decided to offset the rating a bit. The kindle edition really is poor, but I don't think it's fair to rate the entire book so low based off a single edition.

The kindle version is the perfect choice for those of you that enjoys read photocopies done by a bad copier that cannot pick up the thin parts of a letter.

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.

kommt man ohne die Publikationen im Internet alleine mit dem Buch nicht klar. Der eine Autor, Yves Bertot, hat ein PDF veröffentlicht "Coq in a Hurry", HAL Id: inria-00001173, 50 Seiten, das teilweise informativer und eben kompakter ist. Wenn man das Buch liest, sollte man immer den Lambda-Kalkül im Kopf haben. Was ich generell an Coq zu kritisieren hätte ist, dass man nicht oder nicht ohne Weiteres Mathematikbuch-Beweise aus den Coq-Beweisen, die das System teilweise selbständig aus den verfügbaren Sätzen konstruiert, automatisch generieren kann. Im Buch wird solches auch nicht beschrieben Das schränkt die Brauchbarkeit doch sehr ein. Ich habe herausgefunden, dass es verschiedenes Mathematiker-Gruppen gibt, die im Internet einzusehende Beweis- und Definitionsbibliotheken für Coq aufbauen. Diese sind jedoch anscheinend vollkommen undokumentiert und daher auch für Mathematiker kaum zu verstehen.