Post

gabby
@fullmoon.id

The point of formal methods isn't to convince the theorem prover that your proof is correct; it's to convince *other human beings* that you are solving the right problem and that your solution to that problem is correct If nobody understands what you are proving or why then the rest does not matter

10 reposts49 likes

Desert Kickboxer
@desertkickboxer.bsky.social

I remember reading about this with Shinichi Mochizuki, the mathematician who somehow reinvented some aspect of geometry from the ground up, and then published various proofs in such a way that even ten years later people didn't know if they were proved or not

Kari Pahula
@kaol.piperka.net

Even with no human in the loop, it's useful to know that a corner case can't happen. Like for doing optimizations. Soundness proof is type checking one level up. Curry-Howard and all that.