Documentation should only refine types (or why Pin::get_unchecked_mut is a ticking bomb)

language design Unsafe Code Guidelines
37

There is another way to set this all up, and I think it is the way you are proposing. I will use terminology from this article for that.

  • We start with the syntactic type system that Rust has, i.e., what is implemented by the type checker (I include the borrow checker in that).
  • We define a semantic type system that makes precise the invariants maintained by the syntactic type system, and prove its soundness against the syntactic type system.
  • Now we make the semantic type system the "ground truth" and we say that all code, safe and unsafe, must follow the rules of the semantic type system.

This could be done, but I think there are several major and minor problems with that.

  1. [minor] Being "semantically well-typed" only really makes sense as a notion on a safe fn. So it is unclear what (if anything) is require for unsafe fn here. But we need to require something so that the compiler can do its optimizations.
  2. [major] The semantic type system is super complicated. I literally wrote a PhD thesis on it, and there are very few people that fully understand this type system. That basically means that the vast majority of the community is excluded from discussing the actual specification of the rules that Rust programs must follow.
  3. [major] The syntactic type system does not uniquely define the semantic type system. There are many different semantic type systems that all match the same syntactic typing rules. This means there are choices to be made here, and due to point (2), it is hard to have a community-inclusive discussion of those choices. To make things worse, we might not even realize when we are making choices. For example, the model I defined in my thesis excludes Pin.
  4. [major] Due to point (2), very few people will be able to actually understand the precise rules their code has to follow. Even fewer will be able to prove that their code follows the rules. What does the rest do? We would hope they can at least run something like Miri, but with this approach, Miri is impossible. The actual condition for code to be well-defined is "must be well-typed in this semantic type system", and that is very undecidable. There's not even a well-defined notion of "this particular execution trace matches the semantic type system". It's all just hopeless.

Due to all of these reasons, I think this is the wrong approach to follow for Rust. We should not make some semantic type system the basis for defining what the compiler is allowed to assume. Instead, we should have an operational semantics with an explicit notion of UB, and the only assumption the compiler is allowed to make is that code will never hit any of the UB cases in the operational semantics.

I very strongly believe that if the disaster which is UB in C teaches us anything, it is that the only UB we may have in a language is UB that we can test for fully automatically at least on a per-execution basis, i.e., UB which is amenable to a tool like Miri. (This is already de-facto violated be 'relaxed' atomic memory accesses, and that causes me no end of frustration. But at least that is a feature only used by tiny amounts of unsafe code. And once they get the out-of-thin-air problem fixed it should be possible to at least do this in theory, if not in practice, so that's something.)

3 Likes