TBH, I think we need tooling to better help computers help double-check that humans at least considered everything, even if it can't check the proof itself. (Though stuff like kani being able to check the proof would also be nice!)
And my hope is that in doing that, we do it in a way that does allow big-scoped unsafe
blocks again, because it would allow "proving" the thing once, but in a smart way.
Like if you have a local let p: *mut SomethingCopy = ...;
, then there shouldn't be a need for two unsafe blocks if you need to *p = 0;
then *p = 1;
, because the safety considerations are the same. But today there's no way to talk about *p
's without also letting you *q
, so I've been thinking we need some sort of symbolic thing where you could "pass" variables to it, and have those connected to the preconditions of whatever you're calling.
For example, we could have ptr::write
have a writable(p)
predicate that links back to the same rules as https://doc.rust-lang.org/std/ptr/index.html#safety, then if you blah.write(x);
the tool could check that you had a #[safety(writable(blah), reason = "..."]
on the unsafe
block, and that'd let you write
to that pointer in the block, but not do other unsafe things in the block until you also "proved" those things for the other things you try to do.
(And the tool wouldn't have to know what the writable
predicate actually means, just match up the property and variable names from the call and the callee.)