I've come across this a few times - "In Haskell, once can prove the correctness of the code" - Is this true?
One way to prove the correctness of a program is to "calculate" it from its specification. If the specification is also a Haskell program, equational reasoning can be used to transform a (often inefficient) specification into an equivalent (but usually faster) implementation. Richard Bird describes many examples of this approach, one in his functional pearl on a program to solve Sudoku [1]. Jeremy Gibbons gives an introduction to calculating functional programs in his lecture notes of the Summer School on Algebraic and Coalgebraic Methods in the Mathematics of Program Construction [2].
Sebastian