[Haskell-cafe] is proof by testing possible?

[Curt Sampson]

On 2009-11-10 08:24 +0000 (Tue), Conor McBride wrote:

> On 10 Nov 2009, at 05:52, Curt Sampson wrote:
>
> This is sometimes described as the "reflective" proof method: express
> problem in language capturing decidable fragment; hit with big stick.

Well, that's pretty sweet. *And* you get to use a big stick. Who can
argue with that?

> I'm sure there's more to be found here. It smells a bit of theorems
> for free: the strength comes from knowing what you don't.

Yup. But this seems to me to be heading towards keeping proofs with your
code (which we're already doing in sort of a simple way with our type
systems; how long can it be until we're embedding Coq or Agda proofs in
our production Haskell code?). That's heading well away from testing.
(And I approve.)

cjs
-- 
Curt Sampson       <cjs at starling-software.com>        +81 90 7737 2974
           Functional programming in all senses of the word:
                   http://www.starling-software.com