[catnaroek]

With mere “guidelines”, there is no practical, unambiguous way to establish without a shadow of doubt that a function implemented using unsafe Rust upholds the safety guarantees of safe Rust.

So I want a proper formal semantics, maybe not for all of Rust, but at least for a fragment interesting enough to express lifetime and mutability concerns. In particular, I want a formal account of interior mutability.

[steveklabnik]

I hear you! As I said, these things take time.

The interior mutability primitives in the standard library already have a proof, incidentally. Look at the Rust Belt work.