Earlier quoted context omitted.
https://tsz.dev/sound-mode/ This is awesome. Typescript really needs more of this. I hope this gets more publicized and perhaps get adopted by Microsoft. I am not sure you should call it sound mode though. > It is not a mathematical proof of soundness, and it does not make third-party .d.ts files truthful. Here there are two completely unrelated things First, soundness is a mathematical thing (sorry). If something is…
Thank you for the feedback. I think I should rename the "Sound Mode" to something more honest. "Strict" is already taken so I should think of a better name. Making tsz compatible with tsc and making it sound is mathematically impossible. The history of this stuff ( https://hegel.js.org ) is telling. If you really make a sound JS checker, nobody will really use it unless you build an entire ecosystem as big as npm wit…
I don't think this is the problem.
I mean, ok, the first part of the problem is that typescript can't or won't represent at the type level some real world Javascript constructs. But that's understandable since Javascript can get arbitrarily complicated. (you could do a survey on npm and make a type system strong enough for all existing libraries, but this would probably be too complicated to use)
So this is not by itself too bad if, for each instance of non-representable APIs, you wrote a wrapper library that called the bad library but gave you a perfectly good API to work with. Similar to how in Rust you are supposed to wrap unsafe libraries with a safer, higher level API on top. (except it' s not about memory safety, but type safety. but the same reasoning applies, it's just lower stakes since UB is not involved)
Bur the other, more fundamental problem is that for some godforsaken reason, Typescript decided it was okay to lie with types. Some operations return the wrong type rather than a more honest type. This is not caused by the fact that Typescript has to work with libraries in npm, it's entirely self inflicted. Elsewhere in the thread someone gave an example: stringArray[0] has type string when it should be string | undefined.
This (and all other instances of deliberately lying with types) is why Typescript is unsound. Here's a list of things that cause unsoundness (not sure if complete) https://effectivetypescript.com/2021/05/06/unsoundness/
If all those things are patched up, Typescript can be in general mostly sound, even though it has to work with npm libraries and even though you need to trust other people's .d.ts files. To gain full soundness on your application code, you just need to write wrappers to work around the most egregious cases (which should be a minority). Again, the same situation as Rust is supposed to be: it's in general sound but when you need to interact with bad stuff you write a wrapper. (Note: Rust has its shares of unsoundness, but contrary to Typescript, Rust has a plan to eventually patch them up, even if this causes incompatibilities down the line)