Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Lean proved this program correct; then I found a bug

kirancodes.me

Post reply on HN
Print view View original

11–20 of 186 posts

Re: Lean proved this program correct; then I found a bug

#11

Post by butvacuum »

dchftcs wrote: post #8

This is analogous to the fundamental problem of better automation in programming - eventually, the complexity and correctness of of the spec takes over, and if we don't manage that well, creating the spec is not that much less work than the programming part. If your program was for the wrong thing, a proof of it is also wrong.

everybody also ignores that even hello world isn't deterministic anymore. It just doesn't matter to execution if something broke unless it kicks back an error.

although, this is the best example of how quickly a trivality can knock so called "correct" programs over.

Re: Lean proved this program correct; then I found a bug

#12

Post by quantummagic »

gopiandcode wrote: post #7
davesque wrote: post #3

Am I reading the article wrong? It appears that the author did not test the claims of the proof. Wouldn't a "bug" in this case mean she found an input that did not survive a round trip through the compression algorithm? Update: Actually, I guess this may have been her point: "The two bugs that were found both sat outside the boundary of what the proofs cover." So then I guess the title might be a bit click baity.

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 formal verification to ensure there are no bugs.

Re: Lean proved this program correct; then I found a bug

#14

Post by raincole »

ctmnt wrote: post #6

This article’s framing and title are odd. The author, in fact, found no bugs or errors in the proven code. She says so at the end of the article: > The two bugs that were found both sat outside the boundary of what the proofs cover. The denial-of-service was a missing specification. The heap overflow was a deeper issue in the trusted computing base, the C++ runtime that the entire proof edifice assumes is correct. St…

I found the list of articles on this site amusing:

https://kirancodes.me/posts/log-who-watches-the-watchers.htm...

You can see the clickbaitiness increases over time.

Re: Lean proved this program correct; then I found a bug

#15

Post by ernsheong »

Alan Turing already proved with the Halting Problem that reasoning about program correctness is not possible. But we still try.

Wikipedia: [1] Turing proved no algorithm exists that always correctly decides whether, for a given arbitrary program and input, the program halts when run with that input. The essence of Turing's proof is that any such algorithm can be made to produce contradictory output and therefore cannot be correct.

[1] https://en.wikipedia.org/wiki/Halting_problem

Re: Lean proved this program correct; then I found a bug

#17

Post by ashton314 »

ernsheong wrote: post #15

Alan Turing already proved with the Halting Problem that reasoning about program correctness is not possible. But we still try. Wikipedia: [1] Turing proved no algorithm exists that always correctly decides whether, for a given arbitrary program and input, the program halts when run with that input. The essence of Turing's proof is that any such algorithm can be made to produce contradictory output and therefore cann…

> reasoning about program correctness is not possible

Not possible for all problems. We cannot decide correctness (ie adherence to a specification) for all programs, but we can definitely recognize a good chunk of cases (both positive and negative) that are useful.

The Halting Problem itself is recognizable. The surprising result of Turing’s work was that we can’t decide it.

Re: Lean proved this program correct; then I found a bug

#18

Post by jongjong »

Formal proofs can only ever work to validate against requirements... But a major issue with a lot of modern software is that the requirements themselves can be incorrect and some requirements can logically conflict with other requirements... So long as we have non-technical people formulating requirements, we can never have provably correct software.

I've come across issues in the past which weren't actually bugs. For example, the software was behaving exactly as intended but it looked like a bug to a user who didn't understand the nuances and complexities of what was happening.

I also cannot count how many times a non-technical person asked me to implement conflicting functionality or functionality which would have made the UX incredibly confusing for the user.

Re: Lean proved this program correct; then I found a bug

#19

Post by mkl »

ernsheong wrote: post #15

Alan Turing already proved with the Halting Problem that reasoning about program correctness is not possible. But we still try. Wikipedia: [1] Turing proved no algorithm exists that always correctly decides whether, for a given arbitrary program and input, the program halts when run with that input. The essence of Turing's proof is that any such algorithm can be made to produce contradictory output and therefore cann…

We care only about a very small and narrow subset of possible programs, not any arbitrary one. It's possible to solve this kind of problem in large enough classes of program to be useful.

Re: Lean proved this program correct; then I found a bug

#20

Post by raincole »

ernsheong wrote: post #15

Alan Turing already proved with the Halting Problem that reasoning about program correctness is not possible. But we still try. Wikipedia: [1] Turing proved no algorithm exists that always correctly decides whether, for a given arbitrary program and input, the program halts when run with that input. The essence of Turing's proof is that any such algorithm can be made to produce contradictory output and therefore cann…

> a given arbitrary program and input

Keyword emphasis mine.

Post reply on HN