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.

▲

drooby a day ago | parent | next [-]

Let's be more ambitious with the scaffolding and tooling that makes software correct, secure, and easy to reason about.

▲

SoftTalker a day ago | parent [-]

That would be ambitious, since we haven't been able to create those things yet to date.

	▲	Vaushite a day ago \| parent [-]
		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.

▲

budoso a day ago | parent | prev [-]

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?