3 ms·

You could also say that you don't trust the compilers of safe languages, or their unsafe bits, to be correct. The guarantee here is about as strong. But the sit

by pron 7y ago

You could also say that you don't trust the compilers of safe languages, or their unsafe bits, to be correct. The guarantee here is about as strong. But the situation is not binary, and what we want is the cheapest way to at drastically reduce UB, even if you don't believe the guarantee rises to the level of being absolute.

titzer 7y ago
The burden of proof is quite literally on those making claims, not on me to "not trust" them. There are certified compilers with machine-checked proofs of correctness (e.g. CompCert). That is a whole other level assurance than prose proofs and hand-wavy informal reasoning. It is probably true that most "safe" languages have some holes in them; e.g. Java does.
- pron 7y ago
  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 the other.
  - 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.

by pron 7y ago

titzer 7y ago

The burden of proof is quite literally on those making claims, not on me to "not trust" them. There are certified compilers with machine-checked proofs of correctness (e.g. CompCert). That is a whole other level assurance than prose proofs and hand-wavy informal reasoning. It is probably true that most "safe" languages have some holes in them; e.g. Java does.

pron 7y ago
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 the other.
- 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.