3 ms·

Fine, but the same burden exists for both sound static analysis tools and safe languages. There's no reason to doubt the claims of one yet accept the claims of

• titzer 7y ago
  As automated theorem proving and machine-checked proofs are making rapid progress, the burden is increasing. In the beginning, not much was required in the way of proof about a language's type system. Then came systematization and de facto standardization of programming language semantics, along with a standard way of proving things about type systems (typically, small-step semantics, progress and preservation lemmas). Soon, at least in academic papers, it became the norm and almost required to provide formal proofs of type safety. Those languages and systems that lacked proofs often had holes in them. Nowadays, like I alluded to in my original comment, the burden of proof (quite literally) is being ratcheted up even higher, with machine-checked proofs becoming mainstream in academic circles. So in that context, your original comment that these systems are "guaranteed" to be sound is not yet at the level of proof that I would accept. I have reasonable doubts, because dealing with UB in C/C++ is still an open problem.