My most controversial opinion on programming is that static typing is largely overrated. I've been doing software development professionally for around 20 years now, and I've seen no evidence to suggest that static typing plays a significant role in software quality. The dominant factors tend to be the experience of the developer, coding practices, code reviews, testing, and documentation. And while many ideas, such as OO, sound good on paper, they often don't work out as intended in practice. In the early 2000s OO was all the rage, and it was supposed to solve code reuse, encapsulation, and all kinds of problems. The consensus was that OO was the one true way to do things, and every language had to use some flavor of OO. After decades of production use, it's quite clear that OO did not live up to the hype. What we're seeing now with static typing is a similar situation in my opinion.

The reality is that both type disciplines have been around for many decades, and there are literally millions of projects of all kinds out there written in both static and dynamic languages. Despite that nobody has been able to show any statistically significant trends that suggests projects written in static languages have less defects. This article has a good summary of research to date. Some people will argue that this is just something that's too hard to measure, but that's an absurd argument. For example, effects of sleep deprivation on code quality are clearly demonstrated. So, if static typing played a significant role the effects would be demonstrated the same way.

What often happens in discussions around static typing is that people state that static typing has benefits and then try to fit the evidence to fit that claim. A scientific way to approach this would be to start by studying real world open source projects written in different languages. If we see empirical evidence that projects written in certain types of languages consistently perform better in a particular area, such as reduction in defects, we can then make a hypothesis as to why that is. For example, if there was statistical evidence to indicate that using Haskell reduces defects, a hypothesis could be made that the the Haskell type system plays a role here. That hypothesis could then be further tested, and that would tell us whether it's correct or not. In fact, there was a large scale GitHub study that's been replicated. The conclusion was that there is no statistically significant effect associated with static typing.

I think that the fundamental problem with static typing is that it's inherently more limiting in terms of expressiveness because you're limited to a set of statements that can be verified by the type checker effectively. This is a subset of all valid statements that you're allowed to make in a dynamic language. So, a static language will often force you to write code for the benefit of the type checker as opposed to the human reader because you have to write code in a way that the type checker can understand. This can lead to code that's more difficult to reason about, and you end up with logic errors that are much harder to debug than simple type mismatches. People can also get a false sense of confidence from their type system as seen here where the author assumed the code was correct because it compiled, but in fact it wasn't doing anything useful.

At the same time, there is no automated way to check the type definitions themselves and as you encode more constraints via types you end up with a meta program describing your program, and there is nothing to help you know whether that program itself is correct. Consider a fully typed insertion sort in Idris. It's nearly 300 lines long! I could understand a 10 line Python version in its entirety and be able to guarantee that it works as intended much easier than the Idris one.

I also think dynamic typing is problematic in imperative/OO languages because the data is mutable, and you pass things around by reference. Even if you knew the shape of the data originally, there's no way to tell whether it's been changed elsewhere via side effects.

On the other hand, functional languages such as Clojure embrace immutability and any changes to the data happen explicitly in a known context. This makes it much easier to know exactly what the shape of the data is at any one place in your application. Meanwhile, all the data is structured using a set of common data structures. Any iterator function such as map, filter, or reduce can iterate any data structure, and it's completely agnostic regarding the concrete types. The code that cares about the types is passed in as a parameter. Pretty much any data transformations are accomplished by chaining functions from the standard library together, with domain specific code bubbling up to a shallow layer at the top.

Finally, it's worth noting that types aren't the only approach available. Runtime contracts as seen with Spec in Clojure provide a way to create a semantic specification for what the code is meant to be doing, and to do generative testing against it. This approach is much more flexible than a type system, and it can encode semantically meaningful constraints that are difficult to encode using types.