[mushishi]

Could you give me a pointer to a discussion of type soudness in Rust? I recently watched perhaps 3 years old video about Rust where Simon Peyton-Jones asked about this, and Niko Matsakis answered it was ongoing work back then.

Couldn't find anything proper by googling.

[xvilka]

See the work of Iris[1] project. It's open-source[2] and based on Coq, see Rust-related work[3] in particular.

[1] https://iris-project.org/

[2] https://gitlab.mpi-sws.org/iris/iris/

[3] https://gitlab.mpi-sws.org/iris/lambda-rust