> If you adopt the strict definition of "correct", then "more" correct makes no sense, of course.

On the other hand, it's pretty easy to widen the scope of what you're proving correct about a program in such a way as to make it impossible for Haskell to help you. For instance, "accomplish this in O(n)" or "use less than 1 MB" or "in less than 1 second." People usually only concern themselves with the aspects of the implementation that Haskell prioritizes by surfacing as return values. But there are certainly settings where the method used is as important as getting the answer mathematically correct--in fact the rise of NoSQL shows us that there are even situations where doing the wrong thing quickly is better than aborting in the face of unrecoverable errors.