Array covariance is sound because you'll get a runtime error if you try to write to an array of the wrong type.

How is "you'll get a runtime error if you try" any different from the unsoundness described above in TypeScript?

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

The dynamic checks in the Java case are are a well-defined and narrowly-targeted part of the language semantics- you get an exception on mismatched array writes, out-of-bounds access, etc., but when an expression produces a value it always matches its type.

TypeScript defers these kinds of type system violations to the underlying JavaScript engine, which makes things work out (sometimes with an exception, but sometimes just proceeding with a value that doesn't match the expression's type) using precisely the dynamism we wanted to get rid of. And this can leak out and cause arbitrarily-far-away parts of the program not to match their types, either.

> 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.

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

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.