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@starling-software.com> +81 90 7737 2974 Functional programming in all senses of the word: http://www.starling-software.com