Timeline for Example of terminating program that cannot be written in safe Agda
Current License: CC BY-SA 4.0
4 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jul 25, 2025 at 2:35 | vote | accept | zamfofex | ||
| Jul 24, 2025 at 17:32 | comment | added | Naïm Camille Favier |
@zamfofex Conor McBride gives a more direct diagonal argument in this post. I think the argument Jesper had in mind is something like: the evaluator should take a closed term of type "⊥" (the internal bottom type) to a normal form of that type, of which there are none by definition; thus the evaluator at that type has the type ¬ "⊥", which says that Agda is consistent as a logical system.
|
|
| Jul 24, 2025 at 8:33 | comment | added | zamfofex | I’m confused by "we could use it to prove [...] that Agda is sound". If we imagine an Agda typechecker written in Agda, how does that imply "proving bottom is empty"? Our typechecker wouldn’t allow bottom to be proved, but that doesn’t mean we have proved it can’t. I don’t fully understand what "proving bottom has no well typed terms" even means. Also, I think there is still a bit of indirectness on your proof. Which is fine enough, but it incites the question "where would it go wrong if we tried?" As in, where would we "get stuck" and why couldn’t we overcome it? | |
| Jul 24, 2025 at 7:48 | history | answered | Jesper | CC BY-SA 4.0 |