It's a great intellectual position for happy hour at the campus pub. Yet from a practical standpoint, it's hard to see how programming languages requiring more attention to type system will facilitate banging out code for ordinary problems more quickly.
There are times when it is really important to be able to prove code is correct and times when it is enough to just provide a plausible answer. The market for ML on Rails remains without validation.
It's not a free lunch, but damn is it cheap.
This not the same as 'wrong code' in the abstract. The code will run fine if I don't pass in mismatched data, or more generally bad data. And if I am passing in bad data, static typing doesn't give me good answers, it just keeps the program from crashing. Don't get me wrong, there are times when crashing is bad. But there are times when the cost of a runtime error is nominal and the value of flexible code is high.
Static typing trades one type of cognitive overhead for another. The Java program of 500 classes is its manifestation.
Static typing can make "how do I get this to compile?" a design criterion Consider year 2038 problem. In MySQL, various date types are coerced to the timestamp type by design. Otherwise the program would not compile. Compilation takes precedence over problem solving.
But the other context in which we select and choose and construct data types is because a language insists upon it. Here our choices are not based on how to best represent the world, but by how to package our metaphor into a pre-existing schema. The very first time we compile our code, we have been forced by the compiler to crystallize our code based on an early guess.
When a flat roofed building uses scuppers to provide emergency overflow drainage, it is good if water passing through them makes a mess of the plantings below and perhaps stains the facade. It indicates that the primary drains are clogged before the roof collapses. Likewise, runtime type errors might be preferable to zeros silently inserted into a database.
Static and dynamic typing each catch some types of errors at runtime at the expense of masking other types of errors at runtime.
I think types make us write out the why next to the what. That why might be a domain model justification, or something much more trivial. It's also completely possible to encode an untyped regime in a type system. You're always crystallizing your design, you just can either provide good information to understand its failings and be more prepared to fix them. Or not and chase logic errors throughout an undocumented, dynamic system.
And I'd love Bash embedded in a DT. Even if I never write the DT components being able to nicely map Bash -> DT is powerful.
Finally, I'd love Bash with sum types.
I'm not willing to concede that strong static typing is a universal truth though. Too many people much smarter than me seem to disagree.