What I think that is missing from Rust is a way to annotate that a given safe operation provide safety-related guarantees that some unsafe code defined on the same crate relies upon.
For example, if an unsafe code relies upon the field len being less than or equal to capacity, maybe the field should have #[something] on them to warn about this, and every code (even safe code) that modifies those fields needs to be inside some something { .. } block.
This is not the same thing as unsafe { .. } because unsafe blocks have the opposite polarity - unsafe blocks create new demands upon other code that might violate a given invariant (which, due to privacy, we try to generally restrict it to code in the same module - though unfortunately there are unsafe code that relies on global proprieties of the program), that is, unsafe blocks introduce new obligations to other code. This something { .. } I'm talking about would do the opposite, it would fulfill obligations.
(I think this is related to the comment that only unsafe operations have safety preconditions)
Now, naming is hard. I saw here a suggestion that the dual of unsafe should be called robust (even though I don't really understand it at a deeper level, I think it's close to what I'm proposing).
With that in mind, a rough sketch would be something like this
struct Vec<T> {
data: *mut T,
#[robust]
len: usize,
#[robust]
capacity: usize,
}
impl Vec<T> {
pub fn truncate(&mut self, len: usize) {
if len > self.len {
return;
}
unsafe {
// some things..
}
// ROBUST: supposing `self.len <= self.capacity`, and since `len` is
// smaller or equal to it, `self.len` will continue to be smaller or
// equal to capacity
robust {
self.len = len;
}
unsafe {
// other things..
}
}
}
Too verbose? Probably. Looking at the actual Vec implementation there's one improvement that comes to mind: it should be syntactically light to run a robust operation inside an unsafe block, otherwise code becomes too noisy (and noisy code means harder to review and ultimately harder to assess whether it's sound). Maybe using postfix keywords or something.
However, in the site I linked above, it discourages documenting something as robust, which is kind of frustrating because if this term isn't used across the ecosystem the whole concept or something dual to unsafe will continue to be ignored by the Rust community at large.