> "most of the time" being 60%

I would expect this number to get closer to 99% with LLM-based AI code completion tools, so the gap between dynamically-typed languages and "good enough" languages that claim to be statically typed (but are in fact unsound) will become much less significant. But if you want correctness, you will need stronger guarantees.

  > I'd argue that nullability, array covariance, and reflection...

I would mostly agree with that statement, with the caveat that it depends on what you want from your type system. Personally, I want the checker to be (1) sound and (2) decidable and (3) fast. For everything else there's runtime type checking.

  > Type-checkers don't actually need to solve the halting problem to be sound, they just need to guarantee completion for _most_ types of code

Although I don't see much difference between undecidable type systems and dynamically typed languages, as I wrote, I see undecidability as less of an issue. My main concern is unsoundness, which is more critical and unclear how to fix. By "soundness" I specifically mean the formal property that "well-typed programs cannot go wrong". "Most types of code" is just a statistical claim, in which case you might as well use Python or JS/TS with a linter. Too many statically-typed languages decide to go off and roll their own types without reading PL literature, then end up with dealing with these issues later down the line.