Formal methods and TLA+ are a common way of writing verifiable software.
this post was submitted on 16 Feb 2025
46 points (96.0% liked)
Programming
18313 readers
186 users here now
Welcome to the main community in programming.dev! Feel free to post anything relating to programming here!
Cross posting is strongly encouraged in the instance. If you feel your post or another person's post makes sense in another community cross post into it.
Hope you enjoy the instance!
Rules
Rules
- Follow the programming.dev instance rules
- Keep content related to programming in some way
- If you're posting long videos try to add in some form of tldr for those who don't want to watch videos
Wormhole
Follow the wormhole through a path of communities !webdev@programming.dev
founded 2 years ago
MODERATORS
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/
Would this be a consequence of the Project 2025 federal purge?
I was just checking the archives and all captures seem to work that I checked until now. Wondering if they're moving it to WordPress. /s
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).
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.
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.
I was gonna say, if you want formally verifiable, you'd have to go Ada.
Chris Hobbs write a nice book for the context of embedded devices