[Haskell-cafe] Proving correctness

Sebastian Fischer 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 [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].


[1]: http://www.cs.tufts.edu/~nr/comp150fp/archive/richard-bird/sudoku.pdf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20110212/65fc90a5/attachment.htm>

More information about the Haskell-Cafe mailing list