4 ms·

https://tsz.dev/sound-mode/ https://tsz.dev/sound-mode/ This is awesome. Typescript really needs more of this. I hope this gets more publicized and perhaps get

https://tsz.dev/sound-mode/ 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 sound, it's really really sound. Soundness is the thing that says we don't need to manually check the details - we can trust the compiler to do the right thing. It will do the wrong thing if there's a bug, but the implementation can be fixed. Soundness means there's is no bug in the spec, no bug in the type system that would make things go wrong even in theory. Second, and here's the important thing.. it's entirely okay and expected that real world languages need to have unchecked features where we trust the humans to do the right thing, rather than trusting the compiler to verify. That's like Haskell's unsafeCoerce or Java's sun.misc.unsafe. The problem really is when the type system breaks even when we don't do any of those

mohsen1 5mo ago
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 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 with it. TypeScript's decision to embrace existing npm ecosystem and layering .d.ts on top was a very practical decision that made it so successful.
- tialaramex 5mo ago
  > TypeScript's decision to embrace existing npm ecosystem and layering .d.ts on top was a very practical decision that made it so successful. This is basically the same argument made for C++ and I think it's not a very solid one. We know this worked, but that's not evidence that alternatives couldn't have succeeded. I think in a world where Queen never happened the prevailing wisdom would be that someone like Farrokh Bulsara (Freddie Mercury) can't be a rockstar because that seems ridiculous. Actually speaking of royalty, Prince is an even more extreme case. You cannot use numeral-letter substitutions in song titles, that's something for kids and won't... oh unless you're Prince. Yeah, no, "Nothing Compares 2 U" is fine Prince, thanks.
  - mohsen1 5mo ago
    In the Sound Mode page I mentioned that I have some ideas around this. What if we could take .d.ts and project a sound version out of it? How feasible that can be is unclear but the biggest unsoundness criminal is `any` which is relatively safe to project it into `unknown`. And method binvariance stuff are also not impossible to project something more sound out of it. My goal with tsz is to make it practical and useful. I know how difficult it is to convince a tsc user to try something not officially from Microsoft
- nextaccountic 5mo ago
  > TypeScript's decision to embrace existing npm ecosystem and layering .d.ts on top was a very practical decision that made it so successful. 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/ 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)
ngruhn 5mo 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.
- nextaccountic 5mo ago
  > 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

mohsen1 5mo ago

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 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 with it. TypeScript's decision to embrace existing npm ecosystem and layering .d.ts on top was a very practical decision that made it so successful.

tialaramex 5mo ago
> TypeScript's decision to embrace existing npm ecosystem and layering .d.ts on top was a very practical decision that made it so successful. This is basically the same argument made for C++ and I think it's not a very solid one. We know this worked, but that's not evidence that alternatives couldn't have succeeded. I think in a world where Queen never happened the prevailing wisdom would be that someone like Farrokh Bulsara (Freddie Mercury) can't be a rockstar because that seems ridiculous. Actually speaking of royalty, Prince is an even more extreme case. You cannot use numeral-letter substitutions in song titles, that's something for kids and won't... oh unless you're Prince. Yeah, no, "Nothing Compares 2 U" is fine Prince, thanks.
- mohsen1 5mo ago
  In the Sound Mode page I mentioned that I have some ideas around this. What if we could take .d.ts and project a sound version out of it? How feasible that can be is unclear but the biggest unsoundness criminal is `any` which is relatively safe to project it into `unknown`. And method binvariance stuff are also not impossible to project something more sound out of it. My goal with tsz is to make it practical and useful. I know how difficult it is to convince a tsc user to try something not officially from Microsoft
nextaccountic 5mo ago
> TypeScript's decision to embrace existing npm ecosystem and layering .d.ts on top was a very practical decision that made it so successful. 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/ 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)

ngruhn 5mo 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.

nextaccountic 5mo ago
> 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