[Haskell-cafe] is proof by testing possible?

Neil Brown nccb2 at kent.ac.uk
Mon Oct 12 14:31:11 EDT 2009

Dan Piponi wrote:
> On Mon, Oct 12, 2009 at 10:42 AM, muad <muad.dib.space at gmail.com> wrote:
>> Is it possible to prove correctness of a functions by testing it? 
> consider a function of signature
> swap :: (a,b) -> (b,a)
> We don't need to test it at all, it can only do one thing, swap its
> arguments. (Assuming it terminates.)
swap = undefined

Terminates and does not swap its arguments :-)  What do free theorems 
say about this, exactly -- do they just implicitly exclude this possibility?


More information about the Haskell-Cafe mailing list