It’s not like I had a ton of trust in them before, but now they’ve lost almost all credibility.

> At this time, we do not have reason to believe that your Vercel credentials or personal data have been compromised.

Which is not very reassuring without actual information, since presumably they would have said the same thing on Saturday, if asked.

Let me rephrase: aside from that one example from a couple years ago, I haven’t seen any examples of production code written in Lean. I’d be very interested in being proven wrong, this isn’t something I desire, just what I’ve observed. Have you seen any others?

More generally, you implicitly make a good point: writing important libraries in Lean and calling in from another language is probably the most likely use case. So not programs / apps / binaries written in Lean, but small critical components.

Also, part of my confidence comes from both having been a professional programmer for decades, across many languages, and also having programmed in Lean. It’s a great language for math, perhaps the best choice right now. But as a general purpose language it’s incredibly quirky.

Still good to have found, but drawing conclusions past “someone could cheat at proving the continuum hypothesis” isn’t really warranted.

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 scan of lean-lang.org just now, and, other than the two examples I mentioned, didn’t see a single reference to anything other than proving math.

I’m sure you’re in the Lean Zulup, based on what you’ve been up to. Are you seeing people talk about anything other than math? I’m not, but maybe I’m missing it.

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

Still an interesting and useful result to find a bug in the Lean runtime, but I’d argue that doesn’t justify the title. Or the claim that “the entire proof edifice” is somehow shaky.

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, since obviously no one’s running any compiled Lean code in any kind of production hot path.

[1] https://lean-lang.org/doc/reference/latest/Elaboration-and-C...

I used to be sympathetic to complaints about not wanting to pay the developer account fee. But when you’re vibe coding, you’re probably paying a good chunk of change to your LLM supplier of choice every month, and the yearly developer account fee seems minor in comparison

Also, it’s just such a bad security precedent. This page describes the error you get as “the typical macOS Gatekeeper warning”, as though it were just another piece of corporate silliness, like clicking through a EULA.

But I believe you can replace versions on both, nonetheless. It’s a multi step process, unpublish then publish again. But the net effect is the same.