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