A proof of Löb's theorem in Haskell

lesswrong.com

49 pointscubetime2 comments

Interesting to see you can jam something like this into Haskell despite its inappropriateness. The (genuine) Agda proofs are much, much nicer.

Agreed :-)

One of the big questions to me now is whether we can prove the Diagonal Lemma, not just assume it. Do you know if it's possible in Agda? I heard somewhere that it might be hard to find an intuitionistic proof.

Reply on news.ycombinator.com