The author writes:
“This is the web site for a textbook about practical engineering with the Coq proof assistant. The focus is on building programs with proofs of correctness, using dependent types and scripted proof automation.
“I’m following an unusual philosophy in this book, so it may be of interest even to long-time Coq users. At the same time, I hope that it provides an easier introduction for newcomers, since short and automated proofs are the starting point, rather than an advanced topic.”
So I’ve been looking for some kind of accessible guide to programming with dependent types, because I’ve found the existing ATS, Isabelle/HOL, and Coq introductions completely impenetrable. From my glances at the first chapters of this book, though, it seems pretty understandable. Has anyone else read it?