I really loved this introduction to COQ, a formal proof management system which can be used to formalise and prove mathematical theorems. COQ is based on a constructive type theory which allows you to also write dependently typed programs in its formal language, which can be executed by the COQ system itself. COQ’s most famous moment was probably when it was used to formalise the four colour theorem.
This text is available online here, as a series of COQ script files which can be executed and which contain the text of the book as embedded comments. The book itself is really practical, starting quickly with a definition of the semantics of a simple language of expressions over the natural numbers (including times, plus and later comparison), and then proves a the correctness of a compiler that compiles an expression to run on top of a simple stack machine.
The book then rapidly moves on to give an overview of the whole COQ system. It starts with a description of very basic programming and proving, all the while working through a set of examples. It covers infinite data types and the equivalence of streams. It then moves on to issues around programming with dependent types and more general forms of recursion, covering the tricky constructive concepts of equality and universes.
The final section of the book discusses more proof engineering concepts such as using reflection in proofs, and one chapter covers the Ltac language, allowing a user to invent new proof methods (whilst keeping the core logic consistent).
A brilliant book that covers both the theoretical concepts and also explains them with a stream of useful practical examples. Loved it!