[saghm]

> Because the context here is the idea of using the type system to justify removing those sorts of dynamic checks to generate better code

It's more specific than that; the discussion is about writing an ahead-of-time compiler, which necessarily wouldn't be running on a JavaScript engine. The compiler could just as easily emit code that always throws a runtime exception instead of emitting an equivalent to whatever the JavaScript would do.

[Rusky]

A compiler that emitted enough checks to make TypeScript sound would not perform competitively with a JIT, is my point.

[saghm]

Okay, I think I understand now. My intuition was that "soundness" refers to whether the compile catches all invalid usage of types, and that soundness if violated if that doesn't happen; it sounds like the way you're using the term is measured whether the invalid usage is caught either at compile-time or run-time, and soundness if violated if it's not caught by any of the checks. I don't know whether my narrower understanding of soundness is incorrect or not, but it's at least more clear to me now why you grouped Java and JavaScript differently in terms of soundness.