A proof of Löb's theorem in Haskell

Y	Hacker News new \| ask \| show \| jobs

	A proof of Löb's theorem in Haskell (lesswrong.com)
	49 points by cubetime 4287 days ago

1 comments

tel 4286 days ago

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

link

cousin_it 4286 days ago

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.

link