What are some good resources to learn to write very reliable/formally verifiable software?
-
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.
