What I always found interesting was the implication that programs proven correct are also free of logic errors more of the time, and worse, that they are free o

What I always found interesting was the implication that programs proven correct are also free of logic errors more of the time, and worse, that they are free of algorithmic complications. To be fair, the latter point is slowly being addressed, although it rips massive holes in the purity of Haskell and Scheme. I mean, who wants to see explicit tail recursion all the time, or mutable large data structures? But the alternative is slow code. I think that Haskell's forced purity is roughly as good at catching logic errors as the strict typing of C++ or the clean syntax of Python: It catches some stuff, some of the time, but never everything, and never reliably. At some point, the onus is on the programmer to write good code.