Software Foundations

I'd recommend people interested in learning formal methods do not start with things such as Coq or Isabelle/HOL. Most people find the process of learning or using those so difficult that they quit with a potentially-permanent aversion to the term formal verification. In engineering, it's often advised to use best tool for the job esp with highest ROI. So, if you're interested in formal methods, I strongly encourage you to start with so-called, lightweight methods that give a lot of…

I'm taking a formal verification course about this right now using the logical foundations volume. This relies on the Coq proof assistant. From what I've begun to understand, they use 'higher order logic', which really means they can quantify (for all, there exists) over things with cardinalities larger than the countably infinite.

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…