| ▲ | Someone 2 hours ago | |
> 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. | ||
| ▲ | amoss 38 minutes ago | parent | next [-] | |
But is fair to state that the verification was *incomplete*, which is what the article does. | ||
| ▲ | lmm an hour ago | parent | prev [-] | |
The problem was in Lean though, so it seems fair. | ||