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

91–100 of 186 posts

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

#91

Post by necovek »

vntok wrote: post #80
gopiandcode wrote: post #72

Earlier quoted context omitted.

Sorry, I'm not sure I follow. We are talking about bugs in a verified system, that is, in this case, a verified implementation of a zlib-based compression tool. Did it have bugs? yes. Several in fact. I'd recommend reading the article for a detailed listing of the bugs in the tool.

Say you study some piece of software. And it happens that it has an automated suite of tests. And it happens that some files aren't covered by the test suite. And you happen to find a bug in one of those files that were not covered. Would you publish a blog post titled "the XXX test suite proved there was no bug. And then I found one"? It would be a bit silly, right?

A test suite never proves anything except that the code works for the test cases in it.

But yes, it would be equivalent to stating "No tests failed but I found a bug" and one would correctly deduce that test coverage is insufficient.

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

#93

Post by Someone »

gopiandcode wrote: post #9
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…

Repeating myself, 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.…

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

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

#94

Post by tarasglek »

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

sorry to hijack the thread. Really cool post. How long did the whole exercise including porting zlib to lean take?

i have a hard real time system that i would love to try this on, but that's a lot of tools to learn and unclear how to model distributed systems in lean.

also, please add rss so i could subscribe to your blog

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

#95

Post by lmm »

Someone wrote: post #93
gopiandcode wrote: post #9

Earlier quoted context omitted.

Repeating myself, 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.…

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

The problem was in Lean though, so it seems fair.

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

#97

Post by tpoacher »

danparsonson wrote: post #66
gopiandcode wrote: post #9

Earlier quoted context omitted.

Repeating myself, 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.…

We're not speaking about bugs in a verified system so much as writing articles making specific claims about that. Surely if we're at the level of precision of formal verification, it's incumbent upon us to be precise about the nature of a problem with it, no? "Lean proved this program correct and then I found a bug" heavily implies a flaw in the proof, not a flaw in the runtime (which to my mind would also be a compe…

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 technically the problem is the confusion between SI vs binary units and the title should really be "I bought a 0.91 terabit drive and was disappointed it didn't have more capacity", technically you'd be right, but people would rightfully eyeroll at you.

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

#98

Post by UltraSane »

ngruhn wrote: post #54
somat wrote: post #33

Earlier quoted context omitted.

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

I think formal verification brings a bit more to the table. The logical properties are not just a second implementation. They can be radically simpler. I think quantifiers are doing a lot of work here (forall/exists). They are not usable directly in regular code. For example, you can specify that a shortest path algorithm must satisfy: forall paths P from A to B: len(shortest(A,B)) That's much simpler than any actual…

AWS has said that formal verification enables their engineers to implement aggressive performance optimizations on complex algorithms without the fear of introducing subtle bugs or breaking system correctness. It helped double the performance of the IAM ACL evaluation code

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

#99

Post by rhdunn »

Tools like this (formal verification, sparse, etc.) and built-in mechanism (types, generics, RAII, rust's borrow checker) can only verify issues within the scope of that framework. There are also trade-offs and limitations with each type and each implementation.

Type checking allows you to (outside of type casting such as in languages like C/C++ and casting to object for generic containers in Java) verify that an object is of a given type. That allows you to be sure that a well-formed program isn't doing things like putting a random object in a list.

Languages like C#, Scala, and Kotlin improve Java generics by making the generic type of a container or other interface/type part of the type system. This allows generic types of a generic type to preserve the inner type. This makes it possible to implement things like monads and mapping functions to preserve the generic type.

A similar thing is possible with union types, sealed interfaces/traits, etc. that allow you to check and verify the return type instead of defaulting it to a generic object/any type.

Likewise with other features like nullable/non-null annotations (or corresponding nullable type annotations like in Kotlin and recent C# versions).

All of these can be abused/circumvented, but if you keep your code within that framework the compiler will stop that code compiling. Likewise, these solve a limited set of bugs. For example, nullable types can't verify memory management and related bugs.

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

#100

Post by Paracompact »

jongjong wrote: post #25
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…

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?
Post reply on HN