3 ms·
The tongue-in-cheek MOTD of the Agda IRC channel outright says “We last proved false at ...”. Of course, Agda is somewhat unusual because they are kind of maki
by mananaysiempre 3y ago
The tongue-in-cheek MOTD of the Agda IRC channel outright says “We last proved false at ...”.
Of course, Agda is somewhat unusual because they are kind of making up the (very strong) logical theory as they go along instead of having a fixed core logic they could dump proofs in for double-checking, like Coq. On the flip side, Agda actually makes for a halfway usable programming language—unlike Coq.