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

  • ___@lemm.ee
    link
    fedilink
    arrow-up
    1
    ·
    4 days ago

    Right, in effect you break down the possible function states along with a more rigorous form of targeted unit testing.

    I don’t believe they used coq, but the sel4 Linux kernel is one of the most famous formally verified applications/systems.

    https://github.com/seL4/l4v

    The way to beat vulnerabilities is to use formally verified building blocks in my opinion.