|
|
|
|
|
by ngruhn
26 days ago
|
|
I think in the context of type systems, soundness means something like: If type system says, x has type T, then x has type T
TypeScripts type system does not have that property. E.g. by default `stringArray[0]` has type `string` when it should be `string | undefined`.But TypeScript could be sound if you eliminate all these cases. If that's the goal of "SoundMode" then the name sounds fair to me. Not even sure `.d.ts` files are a problem in this regard. They are like axioms/facts. Resolution (from formal logic) is a sound inference rule but you can still derive contradictions from contradicting facts. |
|
Agreed. But it isn't the goal of the sound mode. It's still unsound from a type theory point of view, just with fewer holes