The blurb on the sidebar proclaims Scott's MS experience. It's surprising to see someone with a Microsoft background making this complaint. MS spends more effort than any software company on testing, not only in just plain hiring lots of testers, but also on formal methods. They have some of the top formal methods people in the world doing research for them, and armies of people trying to put that research into practice. Making stuff work is hard, and I'd expect someone who worked for Microsoft to know that.<p>I work for a hardware company. Bugs are really, really, bad. If we find a hardware bug in real silicon, at best, we catch it the moment we get the first chip back, and it means that we have a multiple month delay as we fix it and tape out a new chip, not to mention the cost of throwing away all of the partially fabbed chips we've got, plus the multiple million dollar cost of a new mask set. At worst, we have a recall [1]. We take testing very seriously, and we do a lot more formal verification than most software companies.<p>The only things you can be sure about are things that have been formally verified [2], and the list of things that you can formally verify is tiny. We formally verified our adder. It took months. Then we did the multiplier, which was much harder. It took about the same amount of time because of the experience we gained doing the adder, but it wasn't easy. Division took a lot longer, even with the experience of doing addition and multiplication. To think that we can advance the state of the art of "things that work" from something like a multiplier to a complex piece of software with "care" and our "collective will" seems overly optimistic.<p>Everything's going to be broken for the foreseeable future. Putting more effort into testing and less into features is a difference in degree, not in kind. It won't even prevent articles like this from being written because, if all you want to do is find ten bugs in all the software you use, that's still going to be trivial. Considering how much progress has been made in formal methods since 1970, I expect that finding 10 annoying bugs in all of the software I use will be trivial for my entire lifetime.<p>[1] Well, you don't have to do a recall. AMD had a hardware bug that could be fixed by a patch that degraded performance by 10%. Sun famously didn't include ECC in their L2 cache, which resulted in transient failures for a number of customers, and they made customers sign an NDA before replacing their parts. Guess how much people trusted AMD and Sun afterwards?<p>[2] Even then, you're never really sure. How do you know the formal verification process itself isn't buggy? It's turtles all the way down. I know some folks who were trying to build a formally verified OS, and they stopped using ACL2 after discovering a few bugs in it. After all, how can you trust your proof if the proof system itself has bugs? ACL2 is old and crusty, but that's precisely why it's used for more hardware FV than everything else combined, outside of Intel and IBM (both of whom have their own, excellent, internal tools). It's old enough to have great libraries. There are newer systems that have better architectures, but they don't have anything approaching the same level of library support for hardware. Yet another tradeoff of time to market vs. correctness. It can't be avoided.<p>Say you're an engineer who's worried that ACL2 is too buggy for your company to use. You tell your manager. She points out that maybe five ACL2 bugs are discovered every year, and they get more minor each year, as the system gets cleaned up. Moreover, none of the bugs discovered in the past three years have affected any of your proofs, and you wouldn't expect them to have an effect on any proof techniques you're going to use. So you stick with ACL2. And, because you do, there's a tiny risk of a bug. What does this example have to do with the original post? Bugs come from making little decisions like this. No single decision is sure to cause a problem, or (in a company that's serious about testing) even likely to cause a problem, but multiply that tiny probability by the number of times you have to make a tradeoff and the number of lines of code, and it's a statistical certainty that you'll have bugs.