[dllthomas]

Perhaps Devil's advocate, but my rebuttal would be that we're not necessarily comparing similar gains to correctness as to optimisation, and that perhaps the correctness gains can be better attained another way where the optimisation gains cannot.

(Personally I find a type checker tremendously valuable for communicating with myself - and my team, I suppose - about assumptions being made in other parts of the program, which can probably be accounted "correctness".)