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
Formal methods and TLA+ are a common way of writing verifiable software.
You should look into Coq as it seems to have some good traction.
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?
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.
The way to beat vulnerabilities is to use formally verified building blocks in my opinion.
The NASA secure coding standards are overbearing, obnoxious, over-engineered, and a huge waste of effort.
But they are absolutely correct and the best guidelines I’m aware of.
https://standards.nasa.gov/standard/NASA/NASA-HDBK-2203
https://standards.nasa.gov/standard/NASA/NASA-STD-871913
https://dev.to/xowap/10-rules-to-code-like-nasa-applied-to-interpreted-languages-40dd
I definitely cannot get behind the “no recursion” rule. There are plenty of algorithms where the iterative equivalent is significantly harder and less natural. For example, post-order DFS.
I guess maybe when lives depend on it. But they should be testing and fuzzing their code anyway, right?
EDIT: I can’t even find in the NASA PDF where it mentions recursion.
You can transform any recursive algorithm into iterative pretty easily though; just create a manual stack.
The rule definitely makes sense in the context of C code running in space. Unbounded recursion always risks stack overflow, and they probably don’t have any tooling to prove stack depth bounds (you totally can do that, but presumably these standards were written in the 1500s).
