Let's be more ambitious with the scaffolding and tooling that makes software correct, secure, and easy to reason about.
replyThat would be ambitious, since we haven't been able to create those things yet to date.
replyWe 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.
replyBarring underspecification, and bugs in the verifier.
Who is “we” here? Every company and individual out there? Do you anticipate a solution to these issues you mentioned that would work to solve all the world’s problems?
reply