[Haskell-cafe] is proof by testing possible?
cjs at starling-software.com
Tue Nov 10 11:02:51 EST 2009
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.)
Curt Sampson <cjs at starling-software.com> +81 90 7737 2974
Functional programming in all senses of the word:
More information about the Haskell-Cafe