> A lot of us are making a living mapping real world problems into software solutions. If that mapping is messed up (and it always is to some degree) then the formal correctness of the type system doesn't matter at all.

If I'm understanding you correctly, you're saying statically typed language can't protect against design flaws, only implementation flaws. But implementation flaws are common, and statically typed languages do help to avoid those.

I'm not saying types always model your problem properly! That's not even well specified. I'm saying that "x has type foo" is never wrong if the program typechecks properly. That's totally different, and it means that you can rely on type annotations as being correct, up-to-date documentation. You can also trust that functions are never applied to the wrong number of arguments, or the wrong types; my point is that this guarantees more, in a less expressive way, than specs.