News for hackers. Stuff that matters.

A comment on Lean proved this program correct; then I found a bug. Parent comment

Re:Lean proved this program correct; then I found a bug by IshKebab on Tuesday April 14, 2026 @05:12AM (#47763142)
> if the software you were running was advertised as formally verified as free of bugs.

Nobody should be advertising that. Even ignoring the possibility of bugs in the runtime, there could also be bugs in the verifier and bugs or omissions in the specification. Formally verified never means guaranteed to be free of bugs.

[ Parent | on HN ]
Re:Lean proved this program correct; then I found a bug by gopiandcode on Tuesday April 14, 2026 @09:47AM (#47765616)
As quoted in the article itself, please take it up with the chief architect of the Lean FRO:

> ... converted zlib (a C compression library) to Lean, passed the test suite, and then proved that the code is correct.

> Not tested. Proved. For every possible input. lean-zip

[ Parent | on HN ]
Re:Lean proved this program correct; then I found a bug by IshKebab on Tuesday April 14, 2026 @11:19AM (#47766806)
Yeah well he shouldn't. That looks like slop tbf.
[ Parent | on HN ]