The University of Pennsylvania offers a free series of books called Software Foundations with the following description:
The Software Foundations series is a broad introduction to the mathematical underpinnings of reliable software.
The principal novelty of the series is that every detail is one hundred percent formalized and machine-checked: the entire text of each volume, including the exercises, is literally a “proof script” for the Coq proof assistant.
The series includes Verifiable C, which seems very appealing as a way to avoid some of C’s infamous “footguns.” I haven’t read the series myself, but I might in the future because I like math, logic & programs that do what they’re supposed to do.
Are there any materials that would be good as alternatives or complements to this series?
Edit: Adding the Vercors Wiki to the resources in this thread
Yes, but be warned, formal software verification is proper hardcore. Complicated computer science theories, scant documentations - much of which assumes you have a PhD in the field, and in my experience it’s quite a leaky abstraction. You’ll end up needing to know a lot about the actual implementation of Lean to figure out why some things work and others don’t, in a way that you don’t need to in “normal” languages.
It’s quite satisfying when it works though. Like a puzzle.
I highly recommend this fun “game”: https://adam.math.hhu.de/#/g/leanprover-community/nng4