Post #1460844
2025-12-27 23:29 UTC
@bob_zim @deliverator true. I haven’t played around with any of those cool formally verifiable languages yet, so I wasn’t comfortable asserting that they’re practical for industry use.
Replies (1)
-
@bob_zim@infosec.exchange 2025-12-27 23:51
@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.