What are some good resources to learn to write very reliable/formally verifiable software?
-
I would take a look at LEAN4.
-
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).
-
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
-
Chris Hobbs write a nice book for the context of embedded devices
-
That's kindeof poetic tbh
-
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 was gonna say, if you want formally verifiable, you'd have to go Ada.
-
You should look into Coq as it seems to have the most 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.
-
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.
-
Formal methods and TLA+ are a common way of writing verifiable software.
