Back from #POPL! The Saturday tracks were well worth attending.
Ronald's discussion of gradual type safety vs soundness was my highlight: https://popl20.sigplan.org/details/wgt-2020-papers/5/Gradual-Typing-as-if-Types-Mattered
When talking about soundness, it's important to say exactly what issues you're handling, and the talk explored this.
miniblog.
Related Posts
Superb article on type systems, open vs closed world soundness, and type systems intentionally not offering soundness:
Brilliant, practical talk on implementing a JS type checker: https://youtu.be/MuC8I1JBKv0 (including soundness tradeoffs and flow-based analysis)
Rust nightly is now warning about upcoming changes to the type checker. There are some (obscure) soundness holes: