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

21–30 of 186 posts

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

#21

Post by muraiki »

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…

When you write a recursive function, Lean’s kernel requires a termination proof, unless the function is a partial or marked as unsafe. In those cases, they can’t be used in proofs. https://lean-lang.org/doc/reference/latest/Definitions/Recur...

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

#22

Post by DonaldPShimoda »

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…

> Alan Turing already proved with the Halting Problem that reasoning about program correctness is not possible.

This is so reductive a framing as to be essentially useless [0]. I think maybe you want to learn more about program correctness, formal verification, and programming language semantics before you make such statements in the future.

[0] See, e.g., type-checking.

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

#23

Post by grg0 »

raincole wrote: post #20
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.

That one little word that changes everything in how you interpret the statement.

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

#24

Post by grg0 »

Clickbait 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.

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

#25

Post by jongjong »

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.

Fully agree. I started hitting this bottleneck when I combined a low-code backend I built with Claude Code to generate web applications.

I can build applications rapidly but the requirements and UX are the bottleneck. So much so that I often like to sit on a concept for multiple days to give myself the time to fully absorb the goal and refine the requirements. Then once I know what to build, it snaps together in like 4 hours.

There are a lot of ambiguities which need to be resolved ahead of time. Software engineering becomes a kind of detailed business strategy role.

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

#26

Post by brookst »

porcoda wrote: post #2

I’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 correctness challenge up to the spec (and once we solve that, it’ll be pushed up to the requirements…)

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

#27

Post by minimaltom »

raincole wrote: post #14
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.

Looks like a normal distribution about the chaos mean to me. I appreciate its not everyones cup of tea, but I like this style of writing.

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

#28

Post by nickvec »

grg0 wrote: post #24

Clickbait 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.

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

#29

Post by youknownothing »

I'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 didn't make a mistake in your formal verification? IOW, how do you know your formal verification is bug-free? Answer: you don't. Or if you try to formally verify your formal verification then you're just translating the problem to a new layer. It's just a chain of proofs that is always ultimately based on an unproven one, which invalidates the whole chain.

You can get asymptotically close to zero-bug proof, but you can never get there 100% of the way.

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

#30

Post by grg0 »

nickvec wrote: post #28
grg0 wrote: post #24

Clickbait 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.

And it took them several thousand words to explain what you just said in a sentence.
Post reply on HN