I think if you're writing code from scratch, this doesn't really apply -- I'm talking about prototyping language implementations without any libraries at all, sorta like you would do with OCaml from a textbook (e.g. TAPL by Pierce)
(I'm aware of all the terrible experiences people have with TypeScript in the NPM ecosystem. But TypeScript is a big, mature tool and you can use it in more than 1 way.)
I just noticed the 'deno check' command I'm using turns strict mode on by default, so that's good.
https://deno.land/manual@v1.4.1/getting_started/typescript
All widely used gradual type systems are unsound because they have to interoperate with untyped code, and the dynamic checks to make it sound are too expensive.
But code written from scratch doesn't have that issue. I'd be interested in a counterexample -- is there a code snippet that passes the strict mode of the compiler, and doesn't interoperate with untyped code, but produces an unexpected runtime error?
I guess by "unexpected" I mean that, at runtime, an operation is performed on a value which is not allowed, and the program fails
---
I googled and found this -- https://effectivetypescript.com/2021/05/06/unsoundness/ -- not sure I agree with some points, e.g. array out of bounds isn't unsoundness! The OPERATION is legal, but the data isn't, which isn't something that any type system will tell you.
Similar to divide by zero -- a runtime error does not imply unsoundness.
Also, casts can produce unexpected runtime errors by definition -- that's why they are casts, and you have to opt in! Bad article.
---
I think these are better examples: https://news.ycombinator.com/item?id=15659657
I believe Java has some of those too. Covariance / contravariance is a common source of unsoundness, but definitely not a dealbreaker for me