In practical terms I need a typechecker to write code at anything like the rate I do, with anything like the defect rate I achieve. But that's possibly sophistry. I agree the principle is not quite right (or at least not quite absolute) as stated; using extra power has a high but finite cost, it is occasionally worth using more power than you strictly need if the benefit is high enough.