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 [1]: http://www.cs.tufts.edu/~nr/comp150fp/archive/richard-bird/sudoku.pdf [2]: http://www.comlab.ox.ac.uk/jeremy.gibbons/publications/acmmpc-calcfp.pdf