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

171–180 of 186 posts

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

#171

Post by StilesCrisis »

danparsonson wrote: post #113
amoss wrote: post #108

Earlier quoted context omitted.

What is the program? There are two different answers to this question, and which one is "correct" depends entirely on the context of who is asking it. 1. It's the code that is specific to this program that sits above the run-time layer (internal view, that most programmers would take). 2. It's the code in the binary that is executed (external view, that most users would take). The key question does not seem to be "wa…

Yes but, without wishing to be snarky, did you read the article? There is no program as such, in either sense - the announcement from Lean only mentions "a C compression library" (zlib). Not only that, but since we're talking about formal verification, a programmer would likely understand that that is about proving a bounded, specific codebase at source code level, and not operating on a binary along with its associa…

I am pretty sure you could tell a teenager "there's a ZIP compression program that's scientifically proven to have no bugs" and they'd understand you. People don't have to be CS experts to understand that. (Technically it's Gzip but that's mostly irrelevant to understanding the claim here)

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

#172

Post by MaxBarraclough »

xxs wrote: post #149
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.

Generally if I see 'this' to refer to some unknown part in any title, I'd consider it low quality.

Agreed, it's subtle but it's definitely a form of clickbait-style writing.

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

#173

Post by sn9 »

quantummagic wrote: post #88
gopiandcode wrote: post #73

Earlier quoted context omitted.

It does seem that way doesn't it? But as software bugs are becoming easier to find and exploit, I'm expecting more and more people, including those not "sophisticated enough" to understand and employ formal verification to start using it

> I'm expecting more and more people Then it would help to not introduce any confusion into the ecosystem by using a click-baity title that implies you found a bug which violated the formal specification.

We should not cater to people who make decisions based on titles instead of reading the actual article.

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

#174

Post by jongjong »

Paracompact wrote: post #100
jongjong wrote: post #25

Earlier quoted context omitted.

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…

I'm curious about your learning experience, but what was the nature of your bottleneck, exactly? Was the backend perfectly fine as a backend, but Claude struggled to wire it to a frontend gracefully?

Claude does a great job generating the code. The hard part was the UX like if the app gets complex, then I want a new feature which adds more complexity on top; because of the way the application/UX is designed, it's hard to integrate that feature in a way that's not confusing to the user.

Like for example, I used check boxes to mean "include the records in the result set" but in a different section later in the flow, I have a different but similar looking view/list of records but I just want to use the check boxes to do batch delete but don't want the user to think that this means "include in the result set" in this case. So maybe instead I need a different single checkbox at the top which says "Don't ask for confirmation" so the user can just click on the normal "delete icon" on each row to delete the entries quickly without being prompted... But on the other previous view/list I allow the user to use the check boxes to both include the record but also batch delete using a single small cross at the top... But in the later section I mentioned, I don't want to do this because of the way I designed the flow, it would confuse the user and make it hard for them to track what they're doing and where they made the change (I want the selection step to be in a single place, the current page serves a different purpose). So maybe I need to change the other page as well for consistency... And use the "Don't ask for delete confirmation" approach everywhere? But there's not enough space to fit that text on those other pages...

When you solve all the hard problems, this is what coding gets reduced to. Not a hard problem but it's like lots of small ones like that which keep coming up and your interface ends up with a complex URL scheme and lot of modals and nested tabs.

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

#175

Post by NewsaHackO »

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

OK, so now I see the shadow edit you did for the code source, thanks. Unfortunately, it shows that you are incorrect. For one, the function is a private function and can only be called by local code. Everywhere that the function is called, the size given to it is verified by the program; there is even a note that says it limits the maximum zip file size to avoid a zip bomb. In addition, the code you are quoting isn't even the final code; it is an interim step from what Claude was iterating on. Sucks that this got so much traction, as you are purposely being deceptive in trying to say that this is a bug. You intentionally removed the 'private' keyword in the function signature, as you knew that it would tip off most people to then check when it is actually used.

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

#176

Post by quantummagic »

sn9 wrote: post #173
quantummagic wrote: post #88

Earlier quoted context omitted.

> I'm expecting more and more people Then it would help to not introduce any confusion into the ecosystem by using a click-baity title that implies you found a bug which violated the formal specification.

We should not cater to people who make decisions based on titles instead of reading the actual article.

That's a shitty rationale for click-bait titles. Good titles are for the benefit of people who actually read the articles too.

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

#177

Post by gwern »

spullara wrote: post #10

claude making a statement that sounds impressive but it is actually the first codebase it has ever analyzed. "This is genuinely one of the most memory-safe codebases I've analyzed."

It is definitely not the first codebase an extensively RL-trained Claude has ever analyzed. How do you think it got so good?

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

#178

Post by nickvec »

grg0 wrote: post #30
nickvec wrote: post #28

Earlier quoted context omitted.

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.

Definitely one of my biggest pet peeves with articles / blog posts. There is so much fluff. Just get to the point!

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

#179

Post by tpoacher »

danparsonson wrote: post #119
tpoacher wrote: post #97

Earlier quoted context omitted.

You're technically right, but what things are versus how they're promoted or understood by most people (rightfully or not) often diverges, and therefore such "grounding" articles are useful, even if the wording addresses the perceived rather than the factual reality. By way of analogy, if there was an article saying "I bought a 1Tb drive and it only came with 0.91 terabits", I think if you started explaining that tec…

To be clear, I think the article was fine and the author did some useful work (finding a bug in the runtime of a supposedly provably correct system is indeed a valuable contribution!). I don't agree that it's pedantic to explain why the title feels like a bait-and-switch (and thus does a disservice to the article itself). It's just a bit of feedback for future reference. I take some comfort from being technically cor…

Weeeellll, teeeechnically, I didn't say "technically correct", I said "technically right".

(just kidding xD)

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

#180

Post by danparsonson »

tpoacher wrote: post #179
danparsonson wrote: post #119

Earlier quoted context omitted.

To be clear, I think the article was fine and the author did some useful work (finding a bug in the runtime of a supposedly provably correct system is indeed a valuable contribution!). I don't agree that it's pedantic to explain why the title feels like a bait-and-switch (and thus does a disservice to the article itself). It's just a bit of feedback for future reference. I take some comfort from being technically cor…

Weeeellll, teeeechnically, I didn't say "technically correct", I said "technically right". (just kidding xD)

Haha dammit - I'll lose my membership at this rate
Post reply on HN