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

Really? How? That sounds very interesting, I've got a fair knowledge of basic topology, I'd love to see an application to programming... On Oct 12, 2009, at 1:55 PM, Eugene Kirpichov wrote:

It is possible for functions with compact domain, not just finite.

2009/10/12 Joe Fredette :

...

In general? No- If we had an implementation of the `sin` function, how can testing a finite number of points along it determine if that implementation is correct for every point?

For specific functions (particularly those with finite domain), it is possible. If you know the 'correct' output of every input, then testing each input and ensuring correct output will work. Consider the definition of the `not` function on booleans. The domain only has two elements (True and False) and the range has only two outputs (True and False), so if I test every input, and insure it maps appropriately to the specified output, we're all set.

Basically, if you can write your function as a big case statement that covers the whole domain, and that domain is finite, then the function can be tested to prove it's correctness.

Now, I should think the Muad'Dib would know that, perhaps you should go back to studying with the Mentats. :)

/Joe

On Oct 12, 2009, at 1:42 PM, muad wrote:

...

Is it possible to prove correctness of a functions by testing it? I think the tests would have to be constructed by inspecting the shape of the function definition.

-- View this message in context: http://www.nabble.com/is-proof-by-testing-possible--tp25860155p25860155.html Sent from the Haskell - Haskell-Cafe mailing list archive at Nabble.com.

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

_______________________________________________ Haskell-Cafe mailing list Haskell-Cafe@haskell.org http://www.haskell.org/mailman/listinfo/haskell-cafe

-- Eugene Kirpichov Web IR developer, market.yandex.ru