Re: [Haskell-cafe] is proof by testing possible?

Dan Piponi wrote:

On Mon, Oct 12, 2009 at 10:42 AM, muad 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? Neil.