Dynamic: Loose now —> Strict later
Static: Strict now —> Loose later
Is not strict-to-loose inherently more difficult than loose-to-strict? Perhaps not inherently. Though I can’t imagine how more constraints could increase the expressiveness… Could be my failure of imagination.
But your observation brings up some other question for me:
Is not the base type of everything a 1 or a 0?
Then we have higher composed types like words, ints, longs, etc.
And whether we call them statically typed or not, aren’t all modern languages statically typed in this way? Where the base byte formats are all marshaled, checked and managed by the language, often at compile time?
In that sense, untyped programs would be a subset of typed programs, in the sense of byte-layouts being managed.
Wouldn’t it be unfortunate if, in our high level languages, we still had to always handle marshaling data between byte formats manually?
So it would seem that formal type definitions are extremely useful when a problem domain is well specified / defined, especially when you want to build a rigorous model that can abstract over those minutia internal to that domain, like byte-layouts. In other words, strict typing seems to allow for the creation of more generic, loose abstractions.
If that were true, then it would seem zealotry on the strict typing side would be missing the forest for the trees - types should allow us to abstract over the semantics of the objects they define, not to be imposed on the rest of the universe.
Do those intuitions ring true to you or do you think I’m off base?