If you have a system where the developers often aren’t sure what it does, how to organize the code, aren’t designing for maintainability, etc., static type checking really isn’t going to help you pick up the pieces afterward.
I like static type checking for what it does, but it solves some little problems, not big ones. (And can cause their own little problems.)
In other words, it will help you not break things. Tests are existential proofs of something broken, but types establish a universal proof that something is not broken in specific ways. Tests simply can't replace the properties guaranteed by types.
And types can’t represent the properties shown by tests. Type checking as typically applied only catches the simple problems of feeding the wrong argument into a function.
Mere mortals can’t construct type systems to enforce most definitions of correctness or licenses or performance.
> And types can’t represent the properties shown by tests.
That's not true generally. Dependent types can be used to represent any property that a test might check, and lightweight alternatives can prove a subset [1]. And this makes sense from the type of logical property being established: you can easily turn a universally quantified proposition into an existentially quantification, but going the other way around means checking all possible permutations of values.
However, proving a universally quantification is sometimes (often?) far more difficult than proving an existential quantification, which is why programs have to be structured in a certain way to make them amenable to such proofs.
> Mere mortals can’t construct type systems to enforce most definitions of correctness or licenses or performance.
Type systems always improve performance, so I don't know what you mean by that exactly.
It’s not an either/or. Both types and tests help, for different reasons.
For programming in the large, both should be used. In the long run it’s about saving time that is otherwise wasted on wolf-fencing and hair-pulling; and in getting new developers up to speed faster.
Actually with dependent types you totally can encode proofs that your logic is correct. But I don't really see that trickling down into mainstream programming anytime soon.
I normally don't respond to snark but what the heck I'm feeling festive.
Your stated "big problems":
* developers often aren’t sure what it does
It's easier to understand what code is doing in a strongly typed system. Just trying to find where a method is defined in a dynamic language is often difficult and time-consuming.
* how to organize the code
Strongly typed languages generally encourage better code modularity. Not a panacea, but a help.
* aren’t designing for maintainability
Automatic, safe refactoring is a crucial tool in the maintainability toolkit. Again, not a panacea, but a huge help.
I understand there are always bigger problems, and adopting a strongly typed approach after a mountain of technical debt has already accumulated may not be worth it. And if your developers can't write good, maintainable code regardless of static/dynamic types, that is certainly a bigger problem. But none of this means that static types don't solve big problems, which was the assertion I disagreed with.
I like static type checking for what it does, but it solves some little problems, not big ones. (And can cause their own little problems.)