It's worth noting that the GhostCell and similar patterns are already powerful enough to safely express some code that would normally require pointer manipulation or other unsafe features. Of course GhostCell itself is quite unidiomatic and unintuitive, but adding a more idiomatic annotation syntax seems like it might be a sensible goal.