What are some good resources to learn to write very reliable/formally verifiable software? - Lemmy.World

The University of Pennsylvania offers a free series of books called Software Foundations [https://softwarefoundations.cis.upenn.edu/] 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 [https://softwarefoundations.cis.upenn.edu/vc-current/index.html], 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?