[Haskell-cafe] is proof by testing possible?

Jochem Berndsen jochem at functor.nl
Mon Oct 12 14:52:49 EDT 2009

Neil Brown wrote:
> 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?

Normally, one presumes that "undefined" (id est, calling "error") is
equivalent to looping, except that calling "error" is pragmatically
speaking better: it is nicer to the caller of your function (they/you
get to see a somewhat more descriptive error message instead of 100% CPU
without any results).

Regards, Jochem

Jochem Berndsen | jochem at functor.nl | jochem@牛在田里.com

More information about the Haskell-Cafe mailing list