For the reasons explored in the post, I prefer my type systems optional. It has been my experience and observation that typing in languages follow an 90:10 rule. You get 90% of the gains for 10% of the effort. And the remaining 10% for 9x the effort.
I’m rather happy with the way Python allows me to do the easy ones and/or pick the hotspots.
I’ve worked in exhaustively typed languages, and while it gives a sense of safety, it’s literally exhausting. And, anecdotally, I feel I dealt with more zero divides, subscript woops, and other runtime validation errors than I had in less typed languages.
Not that it matters. Soon, we’ll use semantically vague human language, to prompt, cajole, nudge LLM agents to produce programs that are (lossy) statistical approximations of what might be correct programs.