Typescript has an interesting approach to type checking: it will emit JS even if the code isn't well-typed! https://basarat.gitbooks.io/typescript/docs/why-typescript.html
(This is a nice property of gradual typing: you can run unit tests on refactored code even when some code still uses the old API.)
miniblog.
Related Posts
Most of the gradual type systems I've seen are targetting existing languages: you want to interact with existing libraries that don't have type annotations.
Are there many greenfield languages with gradual types? It's a useful technique in other cases, such as refactoring.
The tradeoffs of type system design, and thinking about a gradual type checker for Elixir:
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.