I don't think that's a fair analogy. At this point, I believe we have pretty good ideas that make it possible to write correct software. Most impressively, there has been progress on creating a completely verified C compiler named CompCert: http://compcert.inria.fr/. This really means "completely verified"---they formalized the semantics both of C and of assembly, and used an automated theorem to prove that the semantics of the generated assembly are the same as the semantics of the source code.
Of course, building (and verifying) CompCert took something like 10 years, so it's certainly not a feasible way to write software yet. Maybe a better analogy would be around the invention of the first airplane---we have a long way to go before everyone's flying in a jumbo jet :)
> I don't think that's a fair analogy. At this point, I believe we have pretty good ideas that make it possible to write correct software. Most impressively, there has been progress on creating a completely verified C compiler named CompCert: http://compcert.inria.fr/. This really means "completely verified"---they formalized the semantics both of C and of assembly, and used an automated theorem to prove that the semantics of the generated assembly are the same as the semantics of the source code.
Note that Compcert has had bugs found in it too. Compcert has a verified core, but it's not a fully verified piece of software.
It's still a lot closer to bug free than almost any other software out there.
Yes, I was referring to the verified parts. To the best of my knowledge, these are bug free -- I believe the bugs were found in an unverified portion of the front-end (which I think was subsequently verified). I think the technique works in principle; it's just very, very expensive.
Analogies are like shopping carts; you can only push them so far before they begin to make an annoying high pitched noise. Your analogy probably works better in the ways that you've explained, though.
Of course, building (and verifying) CompCert took something like 10 years, so it's certainly not a feasible way to write software yet. Maybe a better analogy would be around the invention of the first airplane---we have a long way to go before everyone's flying in a jumbo jet :)