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

141–150 of 186 posts

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

#141

Post by necovek »

thatguysaguy wrote: post #38
youknownothing wrote: post #29

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…

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.

I believe it is rooted in legal proceedings where you are usually not required to in principle because it can be hard and/or impossible.

Eg. it is extremely hard to prove you "weren't there" (eg. at a crime site) if you cannot easily prove you were somewhere else (an affirmative): we do not keep court-admissible record of our whereabouts in case we get suspected of being in a place we were not in.

So it does hold in a number of cases where keeping evidence is required for proof. In software, that evidence would be formal specs and test reports which prove that cases covered with those are indeed working as specced, but provide no proof outside those "specs" (loosely considering an automated test a spec too).

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

#142

Post by necovek »

mr_mitm wrote: post #127
thatguysaguy wrote: post #38

Earlier quoted context omitted.

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.

Also, what even is "a negative"? The following statements are equivalent: "There are no squares with diagonals of different lengths" "All squares have diagonals of equal lengths" Similarly, I can rephrase the statement about the absence of bugs. These are equivalent: "This program has no bugs" "This program always does exactly what it is supposed to do" If you think you can't prove the first statement, then go ahead…

  "This program has no bugs"

  "This program always does exactly what it is supposed to do"
I believe these are not the same in software: bugs are not just wrongly implemented requirements, but also missed requirements or constraints (one can claim these are new features, but the fact that ID looped around at 65536 is going to be called a bug by users).

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

#143

Post by alimw »

kuruczgy wrote: post #79
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…

> It’s important to note that this is the Lean runtime that has a bug, not the Lean kernel, which is the part that actually does the verification (aka proving). [1] So it’s not even immediately clear what this bug would really apply to Well, Lean is written in Lean, so I am pretty sure a runtime bug like this could be exploited to prove `False`. Yes, since the kernel is written in C++, technically it's not the part a…

I think this must be wrong. If the kernel is free of bugs then it's not going to pass a proof of false no matter what the Lean compiler gets up to.

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

#144

Post by eithed »

necovek wrote: post #91
vntok wrote: post #80

Earlier quoted context omitted.

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.

These were my thoughts as well and it's nothing new, I think, regarding testing altogether:

- testing libraries (and in this case - language itself) can have bugs

- what is not covered by tests can have bugs

Additionally would add that tests verify the assumptions of coder, not expectations of the business.

To give benefit to the author - I'd read the article as: having tests for given thing ensures that it does the thing that you built the tests for. This doesn't mean that your application is free of bugs (unless you have 100% coverage, can control entire state of the system, etc) nor that it does the right thing (or that it does the thing the right way)

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

#145

Post by gopiandcode »

ctmnt wrote: post #129
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.…

Hi Kiran, thanks for following up. FWIW, I enjoy your blog and your work. And I do think it was a valuable bug you found; also nice to see how quickly Henrik fixed it. Say more about people running Lean in production. I haven’t run into any. I know of examples of people using Lean to help verify other code (Cedar and Aeneas being the most prominent examples), but not the actual runtime being employed. I took a quick…

Yes, here's a concrete example: https://github.com/leanprover/SampCert This is an implementation of a verified sampler, in lean. Not an embedding in some other language. The implementation itself is in lean, and a python ffi is used to call into the verified implementation. I don't know if AWS is big enough for your standards, but here is at least one example. Besides that, I'm more reporting on the general vibe I have observed from numerous talks at AI4maths workshops at Neurips, at the DARPA AI4Math ExpMath kickoff, etc. People are considering Lean as a serious programming language. Maybe that's surprising to the mathematicians, but as a PL person, I find the language really nicely designed and I can understand why people want to write in it.

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

#146

Post by jmalicki »

cubefox wrote: post #125
jmalicki wrote: post #5

Earlier quoted context omitted.

I have experience with similar things! But that's not saying the proofs are an issue - usually the spec you can reasonably prove in lean or another prover, say TLA+ or Z3 depending on your kind of program - has to be overly simplified and have a lot of assumptions. However, that is powerful. It doesn't mean your program doesn't have bugs. It means this big scary complicated algorithm you think works but are skeptical…

> This has been insanely valuable to me lately. This surprises me. Formal verification so far has been a very niche thing apart from conventional type systems. I didn't think lack of vibe coding was much of a bottleneck in the past. Where do you use it?

Roughly anything that, say, has the complexity of a leetcode medium level problem that isn't already an extremely well known algorithm.

Any moderately complex thread safety thing with a few moving parts (e.g. there are multiple mutexes involved in various parts of the system, verify no deadlocks).

The lack of vibe coding has been a bottleneck for literally everything before.

When I see people say the hate vibe coding, I think "why do you hate formal verification? Because you could be spending your time on formal verification instead of removing "code smells" that don't hurt anything from vibe code."

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

#147

Post by gopiandcode »

ctmnt wrote: post #126
dbdr wrote: post #89

Earlier quoted context omitted.

> obviously no one’s running any compiled Lean code in any kind of production hot path Ignorant question: why not? Is there an unacceptable performance penalty? And what's the recommended way in that case to make use of proven Lean code in production that keeps the same guarantees?

Yes, it isn’t performant. Lean isn’t a language for writing software, though you technically can; it’s a language for proving math.

Where are you coming up with this from? This is awfully confident for a fact you seem to have conjured up without evidence. As far as I am aware, Lean is interested in being used as a programming language (see: https://lean-lang.org/functional_programming_in_lean/) and people are deploying Lean in production: https://docs.aws.amazon.com/clean-rooms/latest/userguide/dif...

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

#148

Post by gopiandcode »

IshKebab wrote: post #123
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.…

> if the software you were running was advertised as formally verified as free of bugs. Nobody should be advertising that. Even ignoring the possibility of bugs in the runtime, there could also be bugs in the verifier and bugs or omissions in the specification. Formally verified never means guaranteed to be free of bugs.

As quoted in the article itself, please take it up with the chief architect of the Lean FRO:

> ... converted zlib (a C compression library) to Lean, passed the test suite, and then proved that the code is correct.

> Not tested. Proved. For every possible input. lean-zip

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

#149

Post by xxs »

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.

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

#150

Post by SAI_Peregrinus »

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…

Or it implies a bug in the specification. The spec differing from the intent is a frequent source of bugs, it doesn't matter what language the spec is written in. Most people have experience with (or have seen news stories about) specification bugs in natural-language specifications: legal loopholes!
Post reply on HN