> If you're writing an application that could kill someone if it crashes, you'd better not be relying on the type system to catch those crashes for you, since it will only catch the most obvious ones.
Safety critical systems are quite different from the vast majority of software systems, and raising them as an example in a general programming argument isn't really fair. There already are safety critical certifications that are mandatory for many aviation and healthcare related applications. They generally utilize heavy testing, model checking, and supporting documentation. Very few commercial industries operate with this much attention to quality, basically because it's too expensive.
The GP had raised them, that's the only reason I commented about this.
You are right though, the standard for that type of software is very different from regular programming.
Still, we shouldn't forget that even the strongest typing can't substitute testing. Most likely, even if you had a formally proved system, which is already much, much more difficult than any other kind of regular software development practice, you would still want some amount of testing to go with that system before putting it in production.
Safety critical systems are quite different from the vast majority of software systems, and raising them as an example in a general programming argument isn't really fair. There already are safety critical certifications that are mandatory for many aviation and healthcare related applications. They generally utilize heavy testing, model checking, and supporting documentation. Very few commercial industries operate with this much attention to quality, basically because it's too expensive.