Hacker Newsnew | past | comments | ask | show | jobs | submitlogin

One of the guarantees that Unsafe Rust makes is that well-formed unsafe code cannot trigger unsoundness in safe code.

In other words: I very rarely write unsafe code myself. When I bring in others’ unsafe code, I use cargo-geiger and siderophile (which I help maintain) to quantify it.



It's not a guaranteed guarantee as far as I can understand.

Or such bugreports would make no sense: https://github.com/denoland/deno/issues/15020


The bug report says exactly what I said: if you don't write well-formed Unsafe Rust, then Rust will not make any guarantees about invariant preservation in Safe Rust.

This is exactly the same as in C++, except stronger: in C++, any piece of well-formed code can violate safe invariants. In Rust, only unsafe code can violate safe invariants, and can only do so if it isn't itself well-formed.


According to the RustBelt paper [0]:

> so long as the only unsafe code in a well-typed λRust program is confined to libraries that satisfy their verification conditions, the program is safe to execute.

I think the main caveat is that IIRC, the RustBelt unsafe rules do not cover ALL uses of unsafe in the wild, they analyze only a subset of Rust as whole, and of course, unsafe usage actually has to obey the rules. But I'm hardly an expert here.

That bug report basically says they broke the unsafe rules and thus the guarantee no longer holds (and there is UB).

[0] https://dl.acm.org/doi/abs/10.1145/3158154




Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: