> 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.
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.