I didn't like the clickbait title. I would have preferred something along the lines of
"Lean proves other program correct but not itself"
Lean proved this program correct; then I found a bug
31–40 of 186 posts
Re: Lean proved this program correct; then I found a bug
#32I’ve had similar experiences with code I’ve proven correct, although my issues were of the more common variety than the overflow issue - subtle spec bugs. (I think the post mentions the denial of service issue as related to this: a spec gap) If you have a spec that isn’t correct, you can certainly write code that conforms to that spec and write proofs to support it. It just means you have verified a program that does…
Been thinking about this a lot recently. I think we need a way to verify the specs. A combo of formal logic and adversarial thinking (probably from LLMs) that will produce an exhaustive list of everything the program will do, and everything it won’t do, and everything that is underspecified. Still not quite sure what it looks like, but if you stipulate that program generation will be provable, it pushes the correctne…
What’s important is to prove useful, high-level properties derived from the specs. The specs of program behavior are just the price of admission.
Re: Lean proved this program correct; then I found a bug
#33I’ve had similar experiences with code I’ve proven correct, although my issues were of the more common variety than the overflow issue - subtle spec bugs. (I think the post mentions the denial of service issue as related to this: a spec gap) If you have a spec that isn’t correct, you can certainly write code that conforms to that spec and write proofs to support it. It just means you have verified a program that does…
Whenever I read an article about formal verification systems there is always that nagging thought in the back of my head. Why can you trust your formal verification system to be bug free but you can't trust the program. should not the chance of bugs be about equal in both of them?
You have a program that does something and you write another program to prove it. What assurance do you have that one program has fewer bugs then the other? Why can one program have bugs but the other can't? How do you prove that you are proving the right thing? It all sort of ties into Heisenberg's uncertainty theorem. A system cannot be fully described from within that system.
Don't get me wrong, I think these are great systems doing great work. But I always feel there is something missing in the narrative.
I think a more practical view is that a program is already a sort of proof. there is a something to be solved and the program provides a mechanism to prove it. but this proof may be and probably is incorrect, as bugs are fixed it gets more and more correct. A powerful but time consuming tool to try and force correctness is to build the machine twice using different mechanisms. Then mismatched output indicates something is wrong with one of them. and your job as an engineer is to figure out which one. This is what formal verification brings to the table. The second mechanism.
Re: Lean proved this program correct; then I found a bug
#34I'll probably get a lot of hate mail for this but here goes nothing... Despite what many people like to claim, you cannot prove that a program has no bugs. That means proving the absence of bugs, and you cannot prove a negative. The best thing you can do is fail to find a bug, but that doesn't mean it isn't there. Before everyone starts blabbing about formal verification, etc., consider this: how do you know that you…
The better look at this is not to prove that you have no bugs is that to prove that a program conforms to a specification that Lean can verify.
Even with the addition of two numbers the execution of a program can be wrong if the CPU has a fault or if the runtime of the program has a bug.
I think you just need to look at why formal verification exists.
Re: Lean proved this program correct; then I found a bug
#35Clickbait title, the proved part of the program had no bugs? As an aside, why can't people just write factually? This isn't a news site gamed for ad revenue. It's also less effort. I felt this post was mostly an insulting waste of time. I come to HN to read interesting stuff.
Is it fair when it comes to formally-verified software to only consider bugs that violate a proof, and ignore everything else?
Formally-verified software is usually advertised "look ma no bugs!" Not "look ma no bugs*" *As long as this complicated chain of lemmas appropriately represents the correctness of everything we care about.
In boating theres often debate of right of way rules in certain situations, and some people are quick to point out that giant tanker ships should be giving way to tiny sailboats and get all worked up about it*. The best answer I've heard: they're dead right! that is to say as right as they are dead (if they didnt yield) lol. In the same vein, I think someone who assumed that a formally-verified software was perfect and got hacked or whatever is going to be a bit wiggly about the whole thing.
* = Technically the rules prioritize the tankers if they are "restricted in ability to maneuver" but everyone loves to argue about that.
Re: Lean proved this program correct; then I found a bug
#36I'll probably get a lot of hate mail for this but here goes nothing... Despite what many people like to claim, you cannot prove that a program has no bugs. That means proving the absence of bugs, and you cannot prove a negative. The best thing you can do is fail to find a bug, but that doesn't mean it isn't there. Before everyone starts blabbing about formal verification, etc., consider this: how do you know that you…
I disagree but the constraints required to get there are probably untenable for most practical applications, so in practice I agree.
Re: Lean proved this program correct; then I found a bug
#37Earlier quoted context omitted.
Hi! Author here. When we speak of bugs in a verified software system, I think it's fair to consider the entire binary a fair target. If a buffer overflow causes the system to be exploited and all your bitcoins to be stolen, I don't think the fact that the bug being in the language runtime is going to be much consolation. Especially if the software you were running was advertised as formally verified as free of bugs.…
> I think it's fair to consider the entire binary a fair target. Yes, it's still very much a bug. But it has nothing to do with your program being formally verified or not. Formal verification can do nothing about any unverified code you rely on. You would really need a formal verification of every piece of hardware, the operating system, the runtime, and your application code. Short of that, nobody should expect for…
I read it as that’s also the point. Adding formal verification is not a strict defense against bugs. It is in a way similar to having 100% test coverage and finding bugs in your untested edge cases.
I don’t think the author is attempting to decry formal verification, but I think it a good message in the article everyone should keep in mind that safety is a larger, whole system process and bugs live in the cracks and interfaces.
Re: Lean proved this program correct; then I found a bug
#38I'll probably get a lot of hate mail for this but here goes nothing... Despite what many people like to claim, you cannot prove that a program has no bugs. That means proving the absence of bugs, and you cannot prove a negative. The best thing you can do is fail to find a bug, but that doesn't mean it isn't there. Before everyone starts blabbing about formal verification, etc., consider this: how do you know that you…
What is up with people saying you cannot prove a negative? Of course you can! (At least in formal settings)
For example it's extremely easy to prove there is no square with diagonals of different lengths. I'm the hard end, Andrew Wiles proved Fermat's Last Theorem which expresses a negative.
That's just a nit though, you're right about the infinite regress problem.
Re: Lean proved this program correct; then I found a bug
#39I'll probably get a lot of hate mail for this but here goes nothing... Despite what many people like to claim, you cannot prove that a program has no bugs. That means proving the absence of bugs, and you cannot prove a negative. The best thing you can do is fail to find a bug, but that doesn't mean it isn't there. Before everyone starts blabbing about formal verification, etc., consider this: how do you know that you…
This comment conflates a number of ideas that obscures its own epistemological point. For example, yes, you can prove a negative (for instance, you can prove there is no largest integer).
The question of who validates the validator is real, but the abstraction of "formal verification" does serve a purpose, like any good mathematical or programming abstraction. Whole classes of bugs are removed; what's left to verify is usually much shorter.
Re: Lean proved this program correct; then I found a bug
#40Clickbait title, the proved part of the program had no bugs? As an aside, why can't people just write factually? This isn't a news site gamed for ad revenue. It's also less effort. I felt this post was mostly an insulting waste of time. I come to HN to read interesting stuff.
Yeah, extremely misleading title even if it is technically true semantically. The phrasing gives the impression that a bug was found in `lean-zip` as part of the proof boundary when it was part of the unverified archive-handling code.
The archive-handling code was in lean-zip, it just seems the verifiers forgot to write proofs for it (still a bug).
Thats not the main finding of the article however. The main bug found was actually in the lean runtime, affecting all proofs using scalar arrays where the size of the array is not bounded.