NASA’s approach is a local optimum: great reliability, for a problem of moderate complexity, with extreme cost and slowness. There are other ways to get more reliable software more cheaply. Anybody here who’s written Haskell code can probably point out one: having a compiler with a really good type-checker has a huge effect on the number of bugs you’re able to write, and it does so without being nearly as lumbering and costly as the NASA-style processes that would be needed to get an equivalent bug reduction.
Another more exotic example is Cryptol, software for writing cryptographic code that has to work correctly. Not only does it do strong type checking, it can take a reference implementation of an algorithm and an optimized hardware implementation, and prove whether or not they have the same results for all inputs. Last I checked, they used it to make some shiny new crypto hardware for Rockwell-Collins. It worked, and they finished the whole thing in about three months, which is really good for this sort of project. If they had NASA’d the problem, they would probably still be working on it.
For people looking for a more lightweight place on the effort-reliability curve, just writing decent unit tests can be a big help. Randomized testing can often do even better, since it uncovers weird twisty corner cases. A lot of the bugs in large mature software like web browsers are uncovered by writing a fuzz testing program to chuck random inputs at them and see what happens. This is a lot easier than going over a large code base with a fine-toothed comb.
NASA’s approach is a local optimum: great reliability, for a problem of moderate complexity, with extreme cost and slowness. There are other ways to get more reliable software more cheaply. Anybody here who’s written Haskell code can probably point out one: having a compiler with a really good type-checker has a huge effect on the number of bugs you’re able to write, and it does so without being nearly as lumbering and costly as the NASA-style processes that would be needed to get an equivalent bug reduction.
Another more exotic example is Cryptol, software for writing cryptographic code that has to work correctly. Not only does it do strong type checking, it can take a reference implementation of an algorithm and an optimized hardware implementation, and prove whether or not they have the same results for all inputs. Last I checked, they used it to make some shiny new crypto hardware for Rockwell-Collins. It worked, and they finished the whole thing in about three months, which is really good for this sort of project. If they had NASA’d the problem, they would probably still be working on it.
For people looking for a more lightweight place on the effort-reliability curve, just writing decent unit tests can be a big help. Randomized testing can often do even better, since it uncovers weird twisty corner cases. A lot of the bugs in large mature software like web browsers are uncovered by writing a fuzz testing program to chuck random inputs at them and see what happens. This is a lot easier than going over a large code base with a fine-toothed comb.