Post #1802958
2026-04-29 20:43 UTC
A lesson about Agda and Rocq's design.
When you design a proof assistant entirely based on “I want this exact code to typecheck because I just KNOW it's fine”, it's hard to be in control of what *other* code typechecks. Beware.
Replies (2)
-
@zwarich@hachyderm.io 2026-04-29 21:24
@jonmsterling@mathstodon.xyz Do you have any links to discussions with an explicit example of this?
-
@jonmsterling@mathstodon.xyz 2026-04-29 20:45
“If we fix this soundness bug, then we break all my code for the last ten years!” That’s called being done a solid by the Mathematics. Embrace it. Delete your code that provably sucks.