Comment by SoftTalker
9 hours ago
Software is already too ambitious. It's beyond our ability to write correctly, reason about or manage securely. When we can get to a point where we don't have a level 10 CVE every other week or millions of people's private information leaked constantly, maybe we can talk about getting more ambitious.
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.
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?