Re:Lean proved this program correct; then I found a bug
by DonaldPShimoda on Monday April 13, 2026 @09:43PM
(#47760262)
> Alan Turing already proved with the Halting Problem that reasoning about program correctness is not possible.
This is so reductive a framing as to be essentially useless [0]. I think maybe you want to learn more about program correctness, formal verification, and programming language semantics before you make such statements in the future.
This is so reductive a framing as to be essentially useless [0]. I think maybe you want to learn more about program correctness, formal verification, and programming language semantics before you make such statements in the future.
[0] See, e.g., type-checking.