Lambda the Ultimate

I'll start with the following statement (which from different perspectives may or may not be considered valid by various parties):

Static Type systems and Dynamic Type systems are the two sides of a single coin.

In the past I have raised a number of questions in this forum regarding types and programming languages that have in the main only been answered by those who have a strongly held viewpoint. I have been spending much time over the last few years considering the viewpoints thus exhibited.

The viewpoints expressed have been one of the following:

Static Type are the best - various reasoning
Dynamic Types are the best - various reasoning
Soft Typing system - amalgamation of the best of both worlds - various reasoning.

What has been unsatisfactory about the answers and the discussions that have ensued is that the subject of real world systems and the real world situations they are deployed in have not been closely examined. By this I mean that hardware related errors, system software related errors and user caused errors (including deliberate attacks) have not been brought into the discussion in relation to how the various kinds of type system can help in these conditions.

Putting aside anyone's particular bent in belief as to which is the best kind of type system for programming languages, my question is:

In what areas do each of the above type systems fail to provide the programmer with the tools (language constructs, abstraction facilities, etc.) to actually deal with real world troubles, problems and conditions?

PLT should be about improving what we can actually do with the computing machinery that we use.

With the wide range of people in this forum, what areas of research are being looked or not looked in this regard?

An example problem is an application that works correctly on a single processor system but exhibits somewhat random behaviour on a dual (or more) processor system due to the seemingly random interactions/responses of a third party library or component.

Please, not interested in ideological wars over this.

It is sometimes claimed in the FP community that explicit representation controls (unboxing) are unnecessary, because a good optimizer can re-arrange the data structures into unboxed forms where appropriate (I disregard hardware interaction for this discussion). Litmus questions here:

1. While there are definite successes here, are they real or are they a case of unrealistic benchmarks? Knowing something of the PL.8 research compiler history on this issue, I am hard pressed to believe that program-wide data restructuring will ever compete comprehensively with human prescription. Both would seem to have their place.

2. Assuming that exclusively compiler-based data structure optimization is realistic, is it feasible in the absence of whole-program analysis (issue: dynamic libraries are not optional in the real world)?

3. Again assuming that exclusively compiler-based data structure rearrangement is realistic, is there a reasonable expectation that we can characterize and specify this type of optimization well enough that independently crafted, conforming compilers will exhibit more or less consistent behavior (may exceed, but will do at least transforms X, Y, and Z)?

4. If the comparative metric is performance compared to C rather than performance compared to non-repr-optimized Haskell/ML/O'Caml, is there any comprehensively credible evidence that compiler-driven repr rearrangement is both good enough and predicable enough (in the eyes of the developer) to render prescriptive specification unnecessary? Is there robust evidence that it isn't sufficient?

   I'll settle for promising partial evidence, provided the approach admits an eventual generalization. I'm aware of TIL, and of Xavier Leroy's paper assessing effectiveness of type-driven unboxing, and of the earlier work on PL.8. The conclusions to date suggest to me that leaving this optimization exclusively to the compiler is not likely to be good enough.

Thoughts and references?