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 Someone on Tuesday April 14, 2026 @01:28AM (#47761607)
> when we speak of bugs in a verified software system, I think it's fair to consider the entire binary a fair target.

I agree, but it’s not fair to imply that the verification was incorrect if the problem lies elsewhere.

This is a nice example of how careful you have to be to build a truly verified system.

[ Parent | on HN ]
Re:Lean proved this program correct; then I found a bug by amoss on Tuesday April 14, 2026 @02:24AM (#47761950)
But is fair to state that the verification was *incomplete*, which is what the article does.
[ Parent | on HN ]
Re:Lean proved this program correct; then I found a bug by lmm on Tuesday April 14, 2026 @01:51AM (#47761746)
The problem was in Lean though, so it seems fair.
[ Parent | on HN ]