I don't think there are many caveats at all, and only a single obvious counterexample (Python). As to "crap software", most of application software these days

I don't think there are many caveats at all, and only a single obvious counterexample (Python). As to "crap software", most of application software these days -- crappy or excellent -- is written in safe languages, and nearly all low-level code is written in unsafe languages, including some of the world's most dependable software, from avionics to OSes. We can say with close to certainty that we can do better than C, but we can also say that full soundness (Idris) is not the answer, so the sweet spot is obviously somewhere in the middle. But we really don't know where exactly -- except that it's not at either end -- or even how wide the sweet spot is (or maybe there are multiple ones, which could be either universally equivalent or dependent on some variables). There's more we don't know about software correctness than what we know -- it's extremely complicated and affected by factors ranging from formal languages and complexity theory to management, economics, psychology, and social psychology -- but we believe noe that the ideas of the 1970s of full soundness being the only path have proven wrong (including an acknowledgment even by Tony Hoare [1]), and, indeed, Rust doesn't adopt soundness fully, and relies on testing, code reviews and other unsound processes as the main means for correctness, like virtually all mainstream programming languages. Anyone who cares about correctness (like me -- https://pron.github.io https://pron.github.io) knows to be very skeptical of any claims for absolute answers, let alone simple ones, on that extremely complex subject. [1]: http://176.9.41.242/docs/math/1996-hoare.pdf http://176.9.41.242/docs/math/1996-hoare.pdf