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

  • Mikina
    2·
    3 days ago

    What would be ELI5 use case of this? It has been almost a decade since I did anything math-formal in college, and I wonder what would be some practical uses or situations is SW dev where you should turn to this language.

    EDIT: I skimmed the intro to Verifiable C, and I think I vaguely understand the idea - do I get it right, that the point is to basically create a formal definition of the function you are writing, i.e if you have a function that takes an array and sorts it, you’d have something like

    For every sequence a and every i, 0 <= i < len(F(a)) -> F(a)i < F(a)i+1

    (Or whatever would the correct formal definition be, I don’t really remember the details, I know I missed some stuff about properly defining the variables, but the idea of the definition should be kind of correct)

    And then you define this formal definiton in CoQ, then somehow convert your code into CoQ code it can accept it as F(a), and CoQ will try to proove formally that the function behavior is correct?

    So, it’s basically more robust Unit Testing that’s backed by formal math proofs?

    • ___@lemm.ee
      1·
      3 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.