I have several times in code review prevented people from marking safe interfaces as "unsafe" because they are "special and concerning", overloading the usage of unsafe is itself dangerous.
For an example, consider Vec::set_len in the standard library. Which only contains safe code, but lets you access uninitialized memory and beyond the length of your allocation by modifying the length field of vector: https://doc.rust-lang.org/src/alloc/vec/mod.rs.html#1264
You might be able to fix this with a lint that looked at a bit more context though, `unsafe fn foo()` in a module (or even crate) with no actually unsafe operations is very likely wrong. Likewise `unsafe fn foo()` which performs no unsafe operations and only accesses fields, statics, functions, and methods that are public.
self.len = new_len;
Seems like you could create a sort of userland-unsafe by using a closed trait[1] and requiring its use on a 'dangerous' method or struct or whatever:
mod my_unsafe {
pub trait MyUnsafe {}
}
pub struct MyUnsafe;
impl my_unsafe::MyUnsafe for MyUnsafe;
pub fn dangerous_function<U: my_unsafe::MyUnsafe>() {}
fn main() {
dangerous_function::<MyUnsafe>()
}
That said I find the named use-case kind of weird. The whole point of the library is to do these unsafe things, so it's kind of silly to be like "don't forget it's dangerous!"
I think an interesting part of unsafe Rust is the interplay between positive and negative polarities (unsafe/safe fn vs unsafe blocks basically) and I think that adding new syntax is the way to leverage this kind of idiom in the new kind of unsafe
The safety benefits of Rust appear when you aren't willing to formally prove all the code you write correct. That's because you only have to prove the unsafe code, plus the memory model, correct in order to guarantee memory safety for the entire program. This is less burdensome than in C, where to do the same you have to prove correctness properties about the specific code that makes up the whole program. Rust makes it easier to prove certain properties about the program (far easier in the case of memory safety), but it was always possible.
In particular, the dirty secret of C verifiers is that they don’t handle pointers all that well. Either you find yourself doing a lot of manual proof work or you have to dramatically simplify the memory model.
In contrast, when verifying safe Rust, the rules of the borrow checker allow us to dramatically simplify the verification work. All of a sudden verifying a manual memory program with pointers (borrows) becomes as simple as verifying a basic imperative language. I’ve been working on a tool: https://github.com/xldenis/creusot to put this into practice
On the other hand, the moment you dive into unsafe, all bets are off and you find yourself wading through the marshes of (weak) memory models with your favorite CSL as your only friend.
Note that there are other tools trying to deal with formal statements about Rust programs. AIUI, Rust developers are working on forming a proper team or working group for pursuing these issues. We might get a RFC-standardized way of expressing formal/logical conditions about Rust code, which would be a meaningful first step towards supporting proof-carrying code directly within Rust.
Not without a formal model of C, and the C standard is only an informal, natural-language text. Rust having memory safety as its express goal (which is basically table stakes for any sort of workable language semantics) means that it's at least realistic to think about a formal semantics for Safe Rust. Then you "just" need to deal with the uncomfortable reality that lots of Safe Rust facilities actually bottom out into Unsafe Rust, which is why it turns out you must care about its semantics too. But the hope is ultimately that the small portion of real-world Rust codebases that's Unsafe Rust might not "infect" the Safe Rust to the point of making verification as practically unworkable as in C.
It seems like it is a long way off from being possible to do that for rust.