News for hackers. Stuff that matters.

A comment on A proof of Löb's theorem in Haskell.

Re:A proof of Löb's theorem in Haskell by tel on Saturday September 20, 2014 @11:03AM (#8344649)
Interesting to see you can jam something like this into Haskell despite its inappropriateness. The (genuine) Agda proofs are much, much nicer.
[ Parent | on HN ]
Re:A proof of Löb's theorem in Haskell by cousin_it on Saturday September 20, 2014 @12:49PM (#8344918)
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.

[ Parent | on HN ]