Richard Gabriel in his arguments why "Objects Have Failed", writes:

And as a result we find that object-oriented languages have succumb to static thinkers who worship perfect planning over runtime adaptability, early decisions over late ones, and the wisdom of compilers over the cleverness of failure detection and repair.

Beyond static types, precise interfaces, and mathematical reasoning, we need self-healing and self-organizing mechanisms, checking for and responding to failures, and managing systems whose overall complexity is beyond the ken of any single person.

Sean McGrath makes similar observations:

PI Calculus, the formalism that underlies some common Business Process Modelling languages, may have an interesting role to play in the static versus dynamic languages debate. Lots of powerful techniques that can be used with PI Calculi involve using higher order concepts such as sending names of ports/channels over links, creating ports on the fly and so on.

This stuff drives the math heads nuts because it makes it hard (impossible?) to formally prove equivalence between calculi.

So it boils down to this - do you want to be constrained in terms of flexibility or provably, formally, "correct" at some probably academic level?

Both intersting and compelling arguments, I will admit, I agree with both of them!  That may sound as a surprise to people who recall my piece on "Static vs Dynamic Typing" debate. I had sided with the "Static" side.  Recall however, my arguments were not for more correctness checking rather it was a realization that being more explicit allows a compiler to do a lot of the thinking for you. That is, the navigation, auto completion, on the fly checking, quick fix capabilities that you find in Eclipse and IDEA tend to outweigh the productivity benefits of any dynamic typed language.   People who program in both environments know this as a fact.

However, I've always advocated a loosely coupled architecture.  If you looked at the table I constructed earlier on "loose couping", you see that flexibility is a motivation at the expense of correctness.  Furthermore, I had earlier talked about "programming in the large", and that our notions of programming in the small do not scale for much larger systems.  In fact, the prescription for this, which I explained earlier, is that a dynamic component model is necessary to manage the complexity of building a large scale system.

Thus, the limits of static reasoning can be found at the boundaries between the one author single machine application and the multiple author distributed agent ecosystem.