Don't forget that you also pay hidden costs when you forgo static proofs. It may be that you need to write more explicit tests by hand, or that you pay for the lack of verification with increased run time errors in production.
On the other hand, we can easily measure the effects of factors like sleep [2], overwork [3], and happiness [4] on code quality. If static typing was an actual factor, we’d see exactly the same kinds of effects.
There’s nothing wrong with enjoying static typing, but there’s simply no evidence that it plays any role past personal preference. Different people solve problems in different ways, and have different pain points. It's entirely possible that each type discipline appeals to different mindsets. That is a value in itself.
[1] https://arxiv.org/abs/1901.10220
[2] https://arxiv.org/pdf/1805.02544.pdf
[3] http://web.archive.org/web/20090824001133/http://www.curt.or...
[4] http://neverworkintheory.org/2014/05/01/happy-sw-devs-solve-...
All I'm saying is that if you forgo static checks to avoid "paying the cost" -- and I do agree they come with a cost -- all you're doing is paying the cost elsewhere. Remember all those people saying "I don't need static types, I just write lots of tests"? That's a cost [1]. Or "I don't need types, I've never had type errors"? That's also a cost, though a more insidious one: ignoring that some of the errors they did get could have been prevented with a use of types they just aren't familiar with.
I'm not arguing that static typing/analysis leads to better quality. I'm arguing that people who don't want to pay its cost actually pay it elsewhere.
To be honest, if pressed I would also argue that I wouldn't want a critical system with the potential to endanger lives to be written in a dynamically typed language. Then again, static types alone wouldn't be suitable either.
----
[1] I knew one guy who didn't write tests either. "I don't need tests because they are a waste of my time: I never make mistakes". Guess where he paid the cost? :P Even then, not even writing tests is also an acceptable tradeoff in some situations!
If you have a specification for what the code is supposed to be doing, and you do specification testing then you will have a high level of confidence regardless of the type discipline. The kinds of errors that will slip through in a dynamic language would necessarily be edge cases and undefined behaviors. These are typically the kinds of bugs that static typing can help you catch.
On the other hand, dynamic typing facilitates features such as hot loading. Just last week my team had a production issue where the service we were using changed the API, and the team managing it didn't notify us. We were able to update the code that talks to the service via the REPL with zero downtime. This is something that would've been a much bigger issue if we had to take the whole system down.
I worked on a research project (a subproject of the project described in this NYT article about Peter Neumann: https://www.nytimes.com/2012/10/30/science/rethinking-the-co...) that experimented with addressing data security and integrity issues using strong types.
For example, writing data to the wrong channel, or reading from the wrong channel, was a type error.
Most of the time, most operations could be statically checked, but sometimes they could not. You might, for example, attempt to send a message to a recipient whose privileges change during transmission. Static checking won't help for such cases; the system needed dynamic checking.
The project used a novel programming language with both static and dynamic typechecking. It specified a hardware platform with tag support for dynamic types.
Mention either static or dynamic typing and a controversy erupts as night follows day between advocates of one and advocates of the other. Why not see the costs and benefits of both? I imagine that the practical answer is that supporting one type discipline costs less in development resources than supporting two, but that doesn't mean that the rejected discipline is therefore wrong and bad.
I liked that the project in question's designers didn't engage in a spurious struggle over static versus dynamic types. They understood that both were valuable, that each offered some benefits that the other didn't, and so they used both.
You need a mix.
Most dynamic types then go on to say why bother at all with static. That's where we disagree. It's dynamic types people that tend to be all or nothing. Where as static type people say use them where it's helps catch the obvious errors, so you don't have to write so many tests.
I also find that runtime contracts as seen in Racket and Clojure provide another interesting approach. From my experience contracts make it much easier to specify actual business constraints.