Unsafe Rust can be (and has been) formally verified to satisfy its Rust type, meaning calling it from safe code can't violate memory unsafety. We don't need to trust manual inspection.
IMHO, this is going a bit too far. Some parts of unsafe Rust have had a model produced that can check some of the invariants required for safe Rust. For example, in my understanding, traits were not modeled at all. Still very promising work, but don't want to overstate it either!
I never said all unsafe Rust code was verified, but we certainly have verified the parts required for stuff like Arc and RwLock beyond reasonable doubt.
You mean, if they were used with dynamic trait objects or unsized types or something? I suppose theoretically there could be some issue, since they aren't modeled yet, but in that case it would almost certainly be a (much more worrisome) issue with the safe part of Rust itself, not the specific unsafe code involved in those types. I don't think any proposal for how to model trait objects, for example, would change the model of how semantic types are defined, it would involve adding new semantic types and new theorems about them.
Cool, then yes, we’re on the same page here, I am just extremely cautious when talking about this. It is true that that stuff would indicate a larger problem, but it’s not like we haven’t discovered unexpected larger problems in the past.
reply