Software Foundations

This appears to be a new edition/refactoring/redesign of the previous version of Software Foundations. I haven't had much time to look through it but it looks like there is new material (volume 3?) (EDIT: found a hosted copy of the old version, at least for now: https://softwarefoundations.cis.upenn.edu/current/toc.html)

The previous version was hosted at http://www.cis.upenn.edu/~bcpierce/sf which now redirects to here.

---

This book is very good for self-study. It teaches you Coq, a formal proof assistant/language. Formally-verified programs can be extracted from these proofs into languages like Haskell and OCaml.