What are some good resources to learn to write very reliable/formally verifiable software?
What are some good resources to learn to write very reliable/formally verifiable software?
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
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
The Software Engineering Handbook PDF appears to just be a single page with a broken link on it; is there an archive for the document that's supposed to be there?
That's kindeof poetic tbh
Sorry about that, I'm seeing the same. Here's the site linked from the Internet Archive
https://web.archive.org/web/20240328153801/https://swehb.nasa.gov/
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).
I would take a look at LEAN4.
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
dwheeler.com has a lot of good links. Also look at learn.adacore.com course in SPARK.
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.
Chris Hobbs write a nice book for the context of embedded devices