Hacker News Reader

Comment by Klasiaster | Hacker News Reader

It doesn't mention unsafe in the README but the website says:

  The first versions of our tools are under development, and target a small but interesting fragment of Rust without unsafe features; in the future, we plan to extend our work to tackle a large portion of the language, including certain patterns of unsafe Rust code.

I wonder if this can be used to prove that unsafe code is memory safe.

View on HN

This is an active research topic in our group. Within unsafe Rust code you lose the guarantees of the Rust ownership type system, which are important for framing (figuring out which parts of the memory _could_ be affected by the given operations). As a result, for e.g. pointer-manipulating unsafe code, the code will probably need to be annotated more heavily, to track which values are "owned" by whom etc.

Nitpick, unsafe doesn't turn off the borrow checker. It just allows you to dereference raw pointers which are the things you must be careful about by reasoning about the actual safety yourself as a programmer. Everything else that uses safe pointers (references and mutable references) remain safe.

But how passing around a (constant) raw pointer is not sidestepping borrow checker? Since the pointer (AFAICT) does need to be borrowed, because it's manifestly immutable, it could be passed into several functions that alter the pointed-at memory in arbitrary order.

Yeah it is sidestepping as you say! The distinction is that if you don't sidestep by dereferencing raw pointers, the borrow check still works. Observe that you can cast as raw pointers in safe rust. What unsafe {} changes is that you can dereference them. The borrow checker still works for regularly borrowed values (&var and &mut var etc). This is probably obvious for Rust users, but I find some people take the "turn the borrow checker off" literally by assuming they won't get lifetime errors if the put an unsafe { } around their code.

It's worth noting that the GhostCell and similar patterns are already powerful enough to safely express some code that would normally require pointer manipulation or other unsafe features. Of course GhostCell itself is quite unidiomatic and unintuitive, but adding a more idiomatic annotation syntax seems like it might be a sensible goal.

Reply on news.ycombinator.com