Charles Stanhope at 2017-06-17T04:14:10Z

While identi.ca was down, I came across an online textbook called

"This electronic book is a course on

The principal novelty of the course is that it is one hundred
percent formalized and machine-checked: the entire text is
literally a script for Coq. It is intended to be read
alongside (or inside) an interactive session with Coq. All the
details in the text are fully formalized in Coq, and most of the
exercises are designed to be worked using Coq."

*Software Foundations*that serves as an introduction to formal methods for software development. The tar file includes a LICENSE file that indicates the book is licensed MIT, which seems odd at first, but then the entire source of the book is meant to be executable. From the preface:"This electronic book is a course on

*Software Foundations*, the mathematical underpinnings of reliable software. Topics include basic concepts of logic, computer-assisted theorem proving, the Coq proof assistant, functional programming, operational semantics, Hoare logic, and static type systems. The exposition is intended for a broad range of readers, from advanced undergraduates to PhD students and researchers. No specific background in logic or programming languages is assumed, though a degree of mathematical maturity will be helpful.Timo Kankare likes this.

I found out about this text from Omega Tau podcast 243: http://omegataupodcast.net/243-formal-specification-and-proof/