> No support for using something like separation logic within Rust itself to verify that unsafe code upholds the invariants that the safe language expects. I t

> No support for using something like separation logic within Rust itself to verify that unsafe code upholds the invariants that the safe language expects. I think this is something we might see in the future. There are a lot of formal methods people who are interested in rust. Creusot in particular is pretty close to doing this - at least for simpler invariants https://github.com/xldenis/creusot https://github.com/xldenis/creusot