(I hope this is not entirely off-topic, please tell me if I’m wrong about this.)
I think this paper is an interesting read for anyone interested in type system design: https://raw.githubusercontent.com/namin/unsound/master/doc/unsound-oopsla16.pdf The Java and Scala type system turned out to be unsound (and I am not talking about the old, well-known issue of covariant array types).
Beyond the general “learn from other people’s mistakes”, I feel like Rust in particular has to be careful not to end up with similar issues. The issue in Java arises from the fact that the type checker assumes that types of in-context variables are well-formed in some sense, and it turns out there is a way to get around that invariant. This reminded me a lot of how Rust treats well-formedness, where e.g. the mere presence of a variable of type &'a &'b T
already gives rise to lifetime constraints that the compiler will freely use. We’ve already seen a soundness bug caused by this implicitness, let’s be on the watch for similar issues.