> It's a pretty nice best-of-both-worlds arrangement

It’s also a worst-of-both-worlds arrangement, in that you have to do the extra work to satisfy the type checker but don’t get the benefits of a compiled language in terms of performance and ease-of-deployment, and only partial benefits in terms of correctness (because the type system is unsound).

AFAIK the Dart team felt this way about optional typing in Dart 1.x, which is why they changed to sound static typing for Dart 2.

Without dependent typing, it's the worst of all worlds anyway. You have to express types, but they aren't expressive enough to not have to also express the same in tests, leaving this weird place where you have to repeat yourself over and over.

That was an okay tradeoff for humans writing code as it enables things like the squiggly line as you type for basic mistakes, automatic refactoring, etc. But that stuff makes no difference to LLMs.