Post #1846751
2026-04-29 20:45 UTC
“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.
Replies (1)
-
@MartinEscardo@mathstodon.xyz 2026-04-29 21:30
@jonmsterling I've been advocating for Agda (in particular) to allow us to choose *which* type theory we want to work with, safely, of course. This is particularly important when I say, in a paper, that I formalized my results (given in mathematical vernacular) in Agda. Of course it is also great to incorporate all sorts of ideas in e.g. Agda, even unsound ones. But the point is that soundness alone doesn't fit my bill. There are all sort of sound systems that are sound alone but unsound when combined. I want a proof assistant that allows me to control what kind of mathematics I am talking about.