Comment by drooby
9 hours ago
Let's be more ambitious with the scaffolding and tooling that makes software correct, secure, and easy to reason about.
9 hours ago
Let's be more ambitious with the scaffolding and tooling that makes software correct, secure, and easy to reason about.
That would be ambitious, since we haven't been able to create those things yet to date.
We have. Languages like Lean and Wuffs associate formal correctness proofs to all code. This is impractical to do by hand, but AI can bruteforce it. If a proof exists at all - if the code is ever able to compile and verify - then it proves the code is correct.
Barring underspecification, and bugs in the verifier.