Type theory is much less than "correct by construction" formal methods. Type theory is great at preventing a whole class of bugs (an operation on a value for which that operation doesn't make sense). But it's inadequate for the larger problem, of whether the operation is the correct one.

Formal methods can ensure that the code matches a formally written spec, for all the aspects of the code that are covered by the formal method. Note well: That's not all aspects of the code. And you have the little problem of (correctly) creating the formal spec. This move the problem up a layer, but the problem doesn't go away.

Even given a formal spec, though, it's my impression that formal methods are s l o w. Does anyone have data on this?