4 ms·

Yes! This is much under appreciated. Usually, it’s just some core calculus of the language that is rigorously specified and the rest is hand waving. There are

Yes! This is much under appreciated. Usually, it’s just some core calculus of the language that is rigorously specified and the rest is hand waving. There are some exceptions like JS. But even Java has the problem that if you just implement what’s in the spec, you won’t be able to run anything meaningful unless you also do things exactly how the JDK would. You can find out what the JDK does by reading its code and writing test cases and I think that’s what folks do, if they want to be compatible. UB and memory safety are orthogonal. If we specified formally and super rigorously that a pointer is an integer and that memory is an array of bytes, we could have a UB-free language but memory safety would still be on fire.

gpderetta 3y ago
Everything is memory safe if your only datatype is uint8_t /s
- pizlonator 3y ago
  Yup :-)
tialaramex 3y ago
> If we specified formally and super rigorously that a pointer is an integer and that memory is an array of bytes, we could have a UB-free language That's PVI (Provenance Via Integers) and it's a performance disaster. If anything in memory might be pointed to, almost all the nice modern optimisations aren't correct. It is really popular with a certain kind of "Portable assembler" programmer, who typically has no idea how the machine actually works, nor how their language is defined but is very confident the nonsense they're writing ought to do what they wanted it to do. So, the "bad" news is that you can't have this, your compiler vendor won't make it, and the "good" news is that you'd have hated it anyway which is why they won't make it.
- lifthrasiir 3y ago
  I don't think it is same as PVI, because i) there are a lot of possible non-determinisms still allowed and thus to be exploited, and ii) the specification will have to require only the observational equivalence anyway because every optimization will be invalid otherwise. It should be definitely possible to define a very precise machine without actually mandating PVI.

gpderetta 3y ago

Everything is memory safe if your only datatype is uint8_t /s

pizlonator 3y ago
Yup :-)

tialaramex 3y ago

> If we specified formally and super rigorously that a pointer is an integer and that memory is an array of bytes, we could have a UB-free language That's PVI (Provenance Via Integers) and it's a performance disaster. If anything in memory might be pointed to, almost all the nice modern optimisations aren't correct. It is really popular with a certain kind of "Portable assembler" programmer, who typically has no idea how the machine actually works, nor how their language is defined but is very confident the nonsense they're writing ought to do what they wanted it to do. So, the "bad" news is that you can't have this, your compiler vendor won't make it, and the "good" news is that you'd have hated it anyway which is why they won't make it.

lifthrasiir 3y ago
I don't think it is same as PVI, because i) there are a lot of possible non-determinisms still allowed and thus to be exploited, and ii) the specification will have to require only the observational equivalence anyway because every optimization will be invalid otherwise. It should be definitely possible to define a very precise machine without actually mandating PVI.