> proving equivalence between programs in such languages is feasible Not in the sense of worst-case time complexity. I'm quite aware of Coq, and Idris, and of

> proving equivalence between programs in such languages is feasible Not in the sense of worst-case time complexity. I'm quite aware of Coq, and Idris, and of Turner's work. They can be used productively if (1) the problem has an good and stable specification, and (2) is inherently sequential, and indeed functional, and (3) doesn't need performance. There are quite a few situations where this is the case, but (1) is almost always a problem in industry. See also the agile/waterfall distinction.