2 ms·
This tldr-counter-tldr discussion is circling around this subtle issue: Unsafe code has a "contaminating" effect on the module it's in. For example, consider th
by oconnor663 9y ago
This tldr-counter-tldr discussion is circling around this subtle issue: Unsafe code has a "contaminating" effect on the module it's in. For example, consider the length of a Vec. That's just an integer. Any method on Vec could change that integer without needing an unsafe block. However, increasing the length incorrectly (for example, past the allocated capacity) will totally cause UB, because unsafe code in other methods of Vec assumes the length is correct. Vec is able to expose a safe API, because the length is a private member, and callers can't set it willy-nilly. But code inside the Vec module needs to be very careful, even when it's not explicitly using unsafe blocks.
- protomikron 9y agoIs it possibly to model that efficiently with a total programming language - or do we need a turing-complete language to write a feature-rich vector (or array, matrix, `Vector a N`, etc.) library? I sometimes wonder if we should maybe invest more in non-turing-complete language research. Obviously Haskell (and Rust) are improvements to the status-quo (critical code can be guarded explicitely via unsafe attributes and written by experts), but maybe this does not go far enough.
- oconnor663 9y agoI'm not sure if this is directly related to what you're thinking about or not, but I think some of Rust's stdlib has been formally verified. It might be that more work in formal verification can get us the guarantees we want, without needing to change the language itself.