3 ms·

I don't think that's a useful distinction here. For context, I often work with high reliability software, including formal methods. What's needed for actual pr

I don't think that's a useful distinction here. For context, I often work with high reliability software, including formal methods. What's needed for actual programs is the ability to say one of two things: A) There is no UB in program X or B) UB in program X cannot lead to a violation of constraint Y The current situation in the C family, whether you're using formal methods or not, is that you cannot generally prove (A) and the time traveling, no-holds-barred results of UB in the spec means that (B) is impossible. While rust doesn't entirely solve this, the fact that those statements are true everywhere except unsafe means that the scope of code you have to manually review is limited to something smaller than "everything".

tialaramex 4y ago
> the fact that those statements are true everywhere except unsafe This is not only a technical feature of Rust's standard library, but perhaps more importantly a cultural feature of Rust's ecosystem. The compiler has no technical problem with your "safe" implementation of Index for your type actually just doing unsafe pointer dereferences internally and trusting users to always pick valid indices, just like C. It's a bad idea, but the compiler is not a cop. However Rust's culture says if you're providing unsafe stuff that must be marked unsafe so that other people don't cut themselves on the sharp edges of your code by mistake. You can imagine with a different culture, you'd end up with popular code that's labelled "safe" but has UB all over the place because the interfaces lie everywhere as an "optimisation" and the community just puts up with it.