Stefan O'Rear wrote:

Personally I like the GADT approach best since it is very flexible and convienient. I have never used a purpose-build computer proof system, but (modulo _|_) it took me less than 10 minutes to answer LoganCapaldo (on #haskell)'s challenge to proof that + was commutative ( http://hpaste.org/522 )

I'm afraid it may be premature to call this a proof. Here's your code

data S x data Z

data Add :: * -> * -> * -> * where AddZZ :: Add Z Z Z AddS1 :: !(Add x y z) -> Add (S x) y (S z) AddS2 :: !(Add x y z) -> Add x (S y) (S z)

add_is_commutatative :: Add a b c -> Add b a c add_is_commutatative (AddZZ) = AddZZ add_is_commutatative (AddS1 a) = AddS2 (add_is_commutatative a) add_is_commutatative (AddS2 a) = AddS1 (add_is_commutatative a)

First of all, where is the coverage proof? Given two numbers, S (S Z) and S Z, how to find their sum using the above code? Someone needs to construct the sequence of Adds, _at run-time_! But where is the proof that the sequence of Add applications expresses all possible ways of computing the sum, and each possible sum can be represented as a sequence of Adds? One may say -- this is so trivial; to which I reply that the original question was trivial as well. If we talk about the formal _proof_, then let's do it rigorously and formally all the way. Also, we can write

main = let x = AddS1 (undefined::Add Z Z (S Z)) in print "OK" main2 = let x = add_is_commutatative (undefined::Add Z Z (S Z)) in print "OK"

but (modulo _|_) That is quite an unsatisfactory disclaimer! From the CH point of view, Haskell is inconsistent as every type is populated. Showing that a function is total is precisely demonstrating that the function is the proof of its type. So, showing the absence of bottoms is precisely making

and the evaluation of 'main' and main2 prints OK. Thus we need to do forcing _all_ the way. But what if we forget some forcing? Incidentally, this is exactly what happened: add_is_commutatative should have been strict. But the code above misses the strictness annotation and still it compiles and seems to work -- and gives one a reason to call it a proof despite the deficiency. I'm afraid I have little trust in the system that permits such lapses. the proof! The problem with GADTs and other run-time based evidence is just that: _run-time_ based evidence and pattern-matching. In a non-strict system, checking that the evidence is really present is the problem on and of itself. BTW, Omega, Dependent ML and a few other systems with GADTs are strict.