Can a compiler prove theorems?

Question

I've read about the Curry-Howard Correspondence. If I got it right, it says that there is a correspondence such that propositions in propositional logic correspond to types, and the proposition is true if the type is inhabited. That a type is inhabited is certainly easiest shown by providing an expression of that type; so proofs correspond to expressions. That's neat; if I have to solve an exercise sheet in propositional logic and am not sure if my solution is correct, I translate my solution into an expression in my favourite programming language and let the compiler check it. If it accepts it, my reasoning was correct.

The sad thing is, I have to come up with the proof. It would be certainly more impressive if the computer could proof it. I.e., a theorem solver should be able to prove a provable expression by repeatedly applying inference rules on the axioms until it reaches the theorem. Termination is, of course, not guaranteed, but if this process terminates, we have a proof.

Can I make a compiler do that for me? I.e., write a program such that the compiler may or may not terminate; if it does not, I learn nothing, but if does, my theorem-program is true.

NB: I guess this is not fun im imperative languages; Haskell-related answers are particularly appreciated.

Answer 1

In Haskell you can use the functionality provided by Data.Type.Equality and Data.Type.Bool to turn the compiler into a theorem prover for simple propositions:

import Data.Type.Equality
import Data.Type.Bool

p1 :: 'True :~: 'True
p1 = Refl

p2 :: Not 'True :~: 'False
p2 = Refl

p3 :: Not (Not 'True) :~: 'True
p3 = Refl

p4 :: ('True || a) :~: 'True
p4 = Refl

-- this fails to compile since the proposition is false
-- p5 :: ('False || a) :~: 'True
-- p5 = Refl

Answer 2

Yes it can and in fact does it all the time. Each successful compilation is a proof that there is no typing error in your program.

Depending on the strength of the type system you can try to coerce it into proving certain theorems. For example in Scala 2.x you could implement integer arithmetic in the type system. I.e. proofs of the form a + c = d.