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 <[email protected]> +81 90 7737 2974 Functional programming in all senses of the word: http://www.starling-software.com _______________________________________________ Haskell-Cafe mailing list [email protected] http://www.haskell.org/mailman/listinfo/haskell-cafe
