[price]

There's nothing arcane or particularly theoretical about soundness. It means that if you have an expression of some type, and at runtime the expression evaluates to a value, the value will always be of that type.

For example if you have a Java expression of type MyClass, and it gets evaluated, then it must either throw (so that it doesn't produce any value) or produce a value of type MyClass: either an instance of MyClass, or of one of its subclasses, or null. It will never produce an instance of some other class, or an int, or anything else that isn't a valid value for the type MyClass.

In addition to helping human readers reason about the code, a sound type system is a big deal for a compiler: it makes it possible to compile the code AOT to fast native code, without inserting a bunch of runtime checks and dynamic dispatching to handle the fact that inevitably some of the types (but you don't know which) are wrong.

The compiler implications are what motivated the Dart language's developers to migrate from an unsound to a sound type system a few years ago: https://dart.dev/language/type-system#the-benefits-of-soundn... so that they could compile Flutter apps AOT. This didn't require anyone to make their code resemble what you'd do in a theorem prover — it just means that, for example, all casts are checked, so that they throw if the value doesn't turn out to have the type the cast wants to return.

TypeScript is unsound because when you have an expression with a type, that tells you nothing at all for sure about what the value of the expression can be — it might be of that type, or it might be anything else. It's still valuable because you can maintain a codebase where the types are mostly accurate, and that's enough to help a lot in reading and maintaining the code.

[afiori]

The key factor is that typescript is not a language, it is a notation system for a completely independent language.

The purpose of typescript is usefully type as much javascript as possible, to do both this and have a sound type system it would require to change javascript.

[price]

Definitely to get the most ergonomic programming experience, while also having a sound type system, you'd need to change some of the semantics of the language.

A prime example is that if you index into an array of type `T[]`, JS semantics mean the value you get back could be undefined as well as a `T`. So to describe existing JS semantics in a sound type system, the type would have to be `T | undefined`, which would be a big pain. Alternatively you could make the type `T` and have that be sound, but only if you make the runtime semantics be that an out-of-bounds access throws instead of returning undefined.