I would say that SPJ was quite right, though. Compare and contrast with Haskell. In Haskell, there are broadly only three cases of unsoundness:
* Infinite loops
* `undefined`
* Abuse of unsafe IO behavior, including monads built on or reducible to IO
Rust's unsoundness bugs are all over [0], and come from so many different angles that they feel indistinct from any other low-level C-like language.
I looked a little into RustBelt; how would it have helped this `Pin` issue? I browsed [1] a bit and it seems like `Pin` would have to have been proven on its own in an ad-hoc way not covered by RustBelt.
* Infinite loops
* `undefined`
* Abuse of unsafe IO behavior, including monads built on or reducible to IO
Rust's unsoundness bugs are all over [0], and come from so many different angles that they feel indistinct from any other low-level C-like language.
I looked a little into RustBelt; how would it have helped this `Pin` issue? I browsed [1] a bit and it seems like `Pin` would have to have been proven on its own in an ad-hoc way not covered by RustBelt.
[0] https://github.com/rust-lang/rust/labels/I-unsound%20%F0%9F%...
[1] https://gitlab.mpi-sws.org/iris/lambda-rust/tree/popl18