The amount of modern languages that think they can solve everything in the type system boggles my mind.
I’m building something in Python right now and the lack of static types is just painful.
That being said, Scala and typescript have really powerful (maybe too powerful?) type systems.
I half remember a recent problem in the AWS TypeScript CDK. I don't know what exactly the Type was, but it was like: You get a SomeFoo from (their) API1 and a BarFoo from (their) API2 - they are called nearly the same, they expose basically the same fields, and you are only interested in one of the fields but there are zero convenience functions and you somehow have to convert between these 2 interfaces for no discernable reason and all you want is a `new BarFoo(someFoo.value)` but value is private. That's when you lose all hope because it's functionally identical to just pass `{"value":someFoo.value}` :)
Even if they're not type errors, if I sit back and think about what the root cause is, it's the type system and dynamic typing.
Addressing an array at null? Type error! Referring to a key that doesn't exist? Believe it or not - not a logic error, that's a type error! If we uses objects or structs that's not possible, but arrays are basically structs with dynamic member ;(
Anything around empty()? Type error. Arithmetic errors? Almost always type errors! Using postfix logic operators? Believe it or not, type error! Anything around DateTime? Usually a type error!
I feel the allure of over typing most in typescript, because it is so flexible to make really complicated types. I see the mistakes most often when JS libraries move from JS to TS. They go overboard with the typing. The code becomes gibberish.
It is impossible how to know if a program will halt without running it, in general terms (Halting problem).
One way to think about the type system is as a less expressive language that is guaranteed to halt. So, it has the pro that we can check properties of the system without running it (IMHO, that is amazing), but it also has the con that it is less expressive (I know, or think I know sometimes, some property holds but you need to express it using the the system) which can be frustrating.