Unsoundness in `Pin`

[Ixrec]

@RalfJung

What makes this particularly interesting is how it interacts with the trait system -- Pin::new / Pin::as_mut cannot really be verified inside the scope of the first RustBelt paper as that does not model the trait system.

Has there been any work on formalizing Rust's trait system? Or some "well-known" reasons why it's impossible or unwise to do so? I didn't see anything about traits in RustBelt.