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.
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 :)
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.
If you really want to work on super high quality stuff, there are fields where that is valuable.
C is awful. Linux is awful. Docker "containers" are awful (i.e. fancy branding around cgroups; no actual 'container' at all unlike solaris zones which did everything properly 10 years ago plus Crossbow networking 5 years ago).
We keep using (and inventing) quick hacks promoted by braggadocious personalities instead of stable infrastructure or proper tooling.
Other pieces of the economic puzzle are things like network effects and lock in. I highly recommend this book: http://amzn.to/1FTa7ib
I've released a couple of things that were tested to exhaustion, so far as anyone knows. One advantage of the event-driven approach is that you can do that.
Ok, you don't want to have a bunch of total bozo developers, or the time to get anything useful done will stretch out to infinity, but still, it's not about just 'being good'.