[rmcclellan]

The power/guarantee trade off isn't a fundamental one, even though in current languages you often have to choose between the two. Creating languages that combine the power of untyped languages with the guarantees of static languages is an active field of research. For example, dependently typed languages, while currently too unwieldy for everyday use, show promise of having both power and guarantees much stronger than Haskell. Now a third, ill-defined axis of "usability" comes into play.

[jerf]

"The power/guarantee trade off isn't a fundamental one, even though in current languages you often have to choose between the two."

It is on the Pareto frontier of the two. Which verges on tautological, but it's still a useful observation. If you can trivially extend the power of a construct while maintaining the same guarantees, the construct was simply broken, and extending the guarantees of a construct without affecting its power means simply that the guarantees were excessively conservative in the first place.

(This can almost be copied and pasted any time anybody claims two properties of a program aren't in conflict, the most common probably being security and ease of programming.)

We may be wrong about where the frontier is... but I doubt we've very wrong.

[nightski]

I may be alone, but I actually feel like I lose power when using say dynamic languages. There is less power of expression. Sure I can do whatever I want, but in reality programming is communication, and I find them much less powerful in that respect.

So using an untyped language only to run an analysis on it later doesn't really seem all that appealing to me, even if it could somehow provide the guarantees of Haskell or dependently typed languages.