[lertn]

This got me intrigued. Is there a soundness proof for the Rust type system?

The only language with such a proof that I am aware of is StandardML. Even OCaml is too complex for a soundness proof.

[Measter]

There was a paper a few years ago[0] was related to proving soundness. That could be what they meant.

[0] https://plv.mpi-sws.org/rustbelt/popl18/paper.pdf