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.