[Haskell-cafe] Proving correctness

[Sebastian Fischer]

>
> 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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/haskell-cafe/attachments/20110212/65fc90a5/attachment.htm>