Will Crichton

The distinction matters b/c the TS designers are only sacrificing completeness of their type system (wrt to goal of no UB), not soundness. I'm also interested in languages that gave up soundness in this sense.

It depends whether you would count a runtime type exception as unsoundness. I think it’s fair to call these similar to segfaults. TS remains “object-safe” at runtime (no buffer overflows) but you can also try to set a field on an integer by accident.

I can't quite see how a segfault is different (in practice) from "undefined is not a function". Is it caught-by-OS vs. caught-by-interpreter that you are noting here?

Putting the PL theory hat on... If Javascript had a formal language semantics, "Undefined is not a function" would be listed as a rule. If C had a formal language semantics, *NULL would not be listed as a rule, i.e. have no semantic meaning defining the behavior.

TypeScript (and also Flow and Closure Compiler) has an unsound type system, because it violates the preservation property: an expression e1 can reduce to an expression e2 with a different type.

Unsoundness happens in many rules (generics, array accesses, computed properties, others), not just in isolated cases, in order to keep the type system relatively simple and be able to type real-world JavaScript.

No, this is no correct. TypeScript and Dart are both unsound became expressions of type Integer do not always produce values of type Integer (or errors). Soundness is not only (or even mostly) about error states.

I agree that the type system doesn't satisfy preservation. But soundness is usually defined as not reaching a stuck state, right? (At least, I double checked TAPL and that's what it says.) And so long as the runtime still has dynamic type checks, the whole system is sound.