[rm82]

>I would argue that the "anything goes" dynamic procedural languages ( like Ruby, Python ) are far more anti-human,

Is it anti-human to be able to interact with the code, and explore what it actually does? A run-time type error is one that has real example data.

The assumption we can write perfect code immediately and easily, or that a type analysis can just guide us through, is not the case. And it's breaks down even worse, when 99% of your code is interacting with systems outside of the scope of the typing system. (database servers, client-side browsers, network connections, file-systems). Dynamically typed language are good fits, when the code is mostly glue-code between multiple systems outside of the scope of any type analysis.

But let's not equate functional programming with static typing.

>in languages that provide a strong theoretic framework for reasoning about code.

You act like many of us are ever writing complicated algorithms. We're not. We're writing simple algorithms that deal with complex structures of information. And in the few cases where the algorithms get so complicated you want your invariants to be formally proven, anything less than a full blown theory prover, will be insuffient anyway.