[Haskell-cafe] Proving correctness
fischer at nii.ac.jp
Fri Feb 11 16:48:35 CET 2011
> 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 . 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 .
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the Haskell-Cafe