Jon Sterling6d ago

Regarding Leo’s post, it was in poor taste but no poorer than anyone who knows him has come to expect. My comment is that I bet Lean is inconsistent too. I don’t know exactly where and how, all I am saying is that I don’t doubt it. These are very sophisticated pieces of software.

In fact, I don’t doubt that those working in the trenches of the FRO could point to some dark corners and examples of unpublicised sources of inconsistency.

This isn’t to dunk on Lean. Bugs can happen, and having a small kernel is a good way to limit their scope! But there are many ways for assurances to fail and this can happen inside and outside the kernel.

Show threadJosh Chen6d ago
@jonmsterling As an aside, Leo's post also forgot to mention the kernel soundness bug found just last year ;) https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Soundness.20bug.3A.20hasLooseBVars.20is.20not.20conservative/near/521286338
Public view of Lean | Zulip team chat

Browse the publicly accessible channels in Lean without logging in.

Zulip
Show threadJon Sterling
@jaycech3n it's also super weird how leo in his prs is really stressing now it's an "adversarial exploit". it's a fucking bug. deal with it. we all make bugs.
Mar 18 at 9:40amWeb
Show threadJosh Chen6d ago
@jonmsterling The anti-PR he uses for Rocq is also an adversarial exploit
Show threadCrazazy @ home6d ago
@jonmsterling @jaycech3n makes it sound like lean is security infrastructure, which miiight be PR for people doing program verification in lean (???), but even then you would have to pull off some next level Jia Tan style supply chain attack at a place where the security of their system actually relies on lean proving it correct and at that point the overlapping area on the venn diagrams is so small I don't think it exists yet
Show threadNoCanDo6d ago
@crazazy @jonmsterling @jaycech3n
Lean is not security infrastructure. It is a theorem prover that can perform symbolic verification of code upto ambient assumptions. Nothing works if your os decides to do something silly like maliciously swap your proof binaries with something trivially true on a file read system call. And this cant be ruled out in a world of windows machines with copilot.
Show threadJon Sterling6d ago
@escape_velocity @crazazy @jaycech3n Strongly agree re: "security infrastructure". Reading those PR threads made me think Leo must have become a real bozo over the years, because it is absolutely wrong to treat these things as "exploits".
Show threadmarkusde6d ago

@jonmsterling @jaycech3n Not to speak for Leo, or justify how terrible his posts usually are, but there is a difference between a bug that (key phrase: can be exploited) to prove false, versus a bug that cannot.

I think you start to think this way when you spend a lot of time making the formal methods pitch to AI VC's, which is exactly what this blog post is anyways lol