Hacker News new | ask | show | jobs
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.

1 comments

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

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