zlacker

[parent] [thread] 2 comments
1. ajross+(OP)[view] [source] 2022-10-03 00:18:58
> That's why Rust has `unsafe`, it's so the programmer has a way to encode logic that they believe is safe but aren't yet able to prove.

That's not the right way to characterize this. Rust has unsafe for code that is correct but that the compiler is unable to detect. Foreign memory access (or hardware MMIO) and cyclic data structures are the big ones, and those are well-specified, provable, verifiable regimes. They just don't fit within the borrow checker's world view.

Which is something I think a lot of Rust folks tend to gloss over: even at it's best, most maximalist interpretation, Rust can only verify "correctness" along axes it understands, and those aren't really that big a part of the problem area in practice.

replies(1): >>kaba0+Fp1
2. kaba0+Fp1[view] [source] 2022-10-03 13:37:14
>>ajross+(OP)
I don’t really get your comment - are you agreeing or disagreeing with parent? Because you seemingly say the same thing.

And continuing on parent’s comment, rust can only make its memory guarantees by restricting the set of programmable programs, while C and the like’s static analysis has to work on the whole set which is simply an undecidable problem. As soon as unsafe is in the picture, it becomes undecidable as well in Rust, in general.

replies(1): >>ajross+C52
◧◩
3. ajross+C52[view] [source] [discussion] 2022-10-03 16:38:03
>>kaba0+Fp1
The parent comment seemed to imply that using unsafe was a failing of the developer to prove to the compiler that the code is correct. And that's not right, unless you view thing like "doubly linked list" as incorrect code. Unsafe is for correct code that the compiler is unable to verify.
[go to top]