Post #1460847
2025-12-27 23:51 UTC
@cwg1231 @deliverator The seL4 kernel is pretty widely used (not as common as VxWorks, but it’s up there). It’s mostly C with a little assembly, and most versions are proven correct against a specification in Haskell using Isabelle. It’s a shining example that C code *can be* written correctly, but also of the lengths to which one must go to ensure this correctness.
Newer languages certainly make big parts of the process easier.
Replies (1)
-
@bob_zim@infosec.exchange 2025-12-28 01:19
@cwg1231 @deliverator It’s just so weird how many software people have never heard of formal verification, and have no idea that you can write software which is provably free of implementation bugs. On top of this, software doesn’t decay like a bridge! It doesn’t wear out like an engine does. Once it’s correct, it’s correct forever (or at least until the specification changes)! That’s should be huge! To me, the fact this isn’t even widely known—let alone striven for—is a sign of how unserious the software industry at large is.