Hacker News Reader

Comment by shasta | Hacker News Reader

> Better monitoring is another. Code review processes. Static analysis. Improved communication. There are many more.

Did you mean this? Or NASA's process? Because I wouldn't characterize any of the above as "good ideas about how to [build correct software]".

Reviewing some of your other comments, I think we fundamentally disagree about how close we are to optimal software development practices. Discussing this in economic terms is like discussing the economic reasons that Columbus didn't go to the moon.

View on HN

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.

Reply on news.ycombinator.com