# Documentation should only refine types (or why Pin::get\_unchecked\_mut is a ticking bomb) **URL:** \ **Category:** Unsafe Code Guidelines\ **Created:** [June 5, 2022, 5:38pm UTC](https://internals.rust-lang.org/t/documentation-should-only-refine-types-or-why-pin-get-unchecked-mut-is-a-ticking-bomb/16749 "2022-06-05T17:38:37Z")\ **Posts on this page:** 1\ **Showing post:** 37
**Author:** ![RalfJung](https://sea2.discourse-cdn.com/flex002/user_avatar/internals.rust-lang.org/ralfjung/32/2415_2.png) [@RalfJung](https://internals.rust-lang.org/u/RalfJung)\ **Post date:** [July 6, 2022, 4:51pm UTC](https://internals.rust-lang.org/t/documentation-should-only-refine-types-or-why-pin-get-unchecked-mut-is-a-ticking-bomb/16749/37 "2022-07-06T16:51:15Z")
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](https://iris-project.org/pdfs/2021-rustbelt-cacm-final.pdf) 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](https://research.ralfj.de/phd/thesis-screen.pdf), 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](https://github.com/rust-lang/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.) --- _[View the full topic](https://internals.rust-lang.org/t/documentation-should-only-refine-types-or-why-pin-get-unchecked-mut-is-a-ticking-bomb/16749)._