I don't disagree, but most statically typed languages don't enforce a level of correctness where this would be an issue. We're not programming with theorem prov

I don't disagree, but most statically typed languages don't enforce a level of correctness where this would be an issue. We're not programming with theorem provers with an elaborate specification. I somewhat agree with your point #2 which is why Haskell provides a deferred type checking mode for prototyping purposes[1]. I think this should be more common among typed languages, but this is not a very typical scenario either. [1] https://downloads.haskell.org/ghc/latest/docs/users_guide/exts/defer_type_errors.html https://downloads.haskell.org/ghc/latest/docs/users_guide/ex...