4 ms·

Will there ever be a formal semantics for unsafe Rust?

• steveklabnik 8y ago
  Depends on what you mean by “formal”, and on what timescale, but this group will be a consumer of the “unsafe guidelines WG”, and we would eventually like to formalize such a thing. Some of the participants in this WG would be the ones interested in doing this work. In open source, some people wear many hats :)
  • catnaroek 8y ago
    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 8y ago
      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.