Comment by stygianguest

Only proofs in 'constructive' logic. There's a lot of proofs that aren't executable. Most importantly proofs by contradiction.

See: http://en.wikipedia.org/wiki/Intuitionistic_logic

In practical terms, however, this isn't a huge hurdle and comes with the nice advantage that you always have a program.

BTW. I'm kinda sure you know this already, but I think it is important to mention.

Thanks for the Haskell proof-book link. I'll check it out sometime.