Lean proved this program was correct; then I found a bug.

[-]

programming-ModTeam@reddit

[April Trial] No LLM-related posts. See this post.

[-]

honestly formal verification is wild but yeah this is why i dont trust it for anything critical yet. had a similar thing happen with a rust program where the type system "guaranteed" safety but i still had a logic bug that corrupted data. proof systems are getting better but theyre still just checking what you told them to check, not what you actually meant lol

[-]

notfancy@reddit

proof systems are getting better but theyre still just checking what you told them to check

A proof that your "function" f satisfies ∀x . f⁻¹(f(x)) = x packs a lot of punch.

[-]

comrade_donkey@reddit

I think what OP is trying to say is that if the strongest-postcondition of f is weak, then such a proof is weak, too.

[-]

Zarigis@reddit

While impressive, I would never consider this to be a formally verified compression tool. Just because it can reverse its own output, doesn't mean it has properly followed the standard for the format.

[-]

BadatCSmajor@reddit

One of the few comments so far that actually understands formal verification

[-]

gredr@reddit

Next you'll be saying that just because my unit test is green, that doesn't mean that assert(true) proves my program works correctly. That's not very TDD of you.

[-]

aookami@reddit

Well, this only holds valid in perfect environments. A inverse of a function will never return the function argument if I put a bullet in the processor during runtime

[-]

BadatCSmajor@reddit

Your code can’t go wrong, huh? What if I shoot the computer? What then? Huh? Checkmate, type theorists.

[-]

aookami@reddit

You can also spank it and call it bad silicon

[-]

notfancy@reddit

That's not a bug, that's a felony.

[-]

yawaramin@reddit

The type system 'guarantees' certain kinds of safety, not freedom from logic bugs like using < when you meant to use >.

[-]

Zarigis@reddit

The advantage of formal verification is that it lets you focus your testing on the pieces that aren't verified, it well never replace the need for testing.

[-]

DSrcl@reddit

Read the article before jumping to your conclusion.

Across 105 million executions, the application code (that is, excluding the runtime) had zero heap buffer overflows, zero use-after-free, zero stack buffer overflows, zero undefined behaviour (UBSan clean), and zero out-of-bounds array reads in the Lean-generated C code.

The bug comes from unverified trusted code.

[-]

sistersinister@reddit

I appreciated the apology for the AI-slop quoted in the article.