De Moura was asked why he is so protective of the core of Lean, the proof assistant he created, and won't merge whatever the community submits. He is passing on a colleague's line to explain it: half-finished features that look like they work are the danger in software other people rely on to verify proofs.
Yes, yes. I mean, I remember last year, Ila Sergei is a professor in Singapore. He was with his student Vova, and they demoed something to me. I said, why are these folks demoing this stuff? This is not Ling. And it was really cool, the demo. At the end, they said, no, no, this is Ling. This is an extension we implemented on top of Ling. I was really surprised. It was for software verification. They have a language that's much easier for people to verify software, especially if it's imperative software. Yeah, I was really blown. Yeah, they blew me away, I mean, with the demo.
It's part of the reason that you are so kind of protective over the core. I mean, if you think about it, the reputation of Lean is paramount because this is something that is going to be used to verify software and mathematics and so on. So there's that. But it reminds me a bit of, you know, MATLAB or maybe Mathematica. It has insanely optimized core libraries for doing linear algebra and so on. But someone could come along and they, you know, with great power comes responsibility, they could just make a mess of it. So they could do some operations and it's no longer vectorized and it's really slow. And perhaps in Lean, they could do something that actually affects the integrity of what they're doing. Is that part of it? So you want to put a little bit more control in?
Yeah, there is that. I mean, there's also people adding something that's half-baked. A lot of people like to have fun implementing software. Software is only, I like to see, actually, one of my academic brothers, he says, software is only fun if the software doesn't have to work. If it has to work, the fun disappears very quickly. And first issue, bugs, like you mentioned, people introducing bugs. Second issue, someone submits a feature that's not fully implemented. There are many holes. It looks like it works, but it doesn't. That's the thing. People may lock the design. They add a feature. It's complete. It's correct. But put constraints on how we can optimize the system. And now we have this feature. It may become popular and prevents us from doing other things that are more important because it's there. People use it. We can't easily remove it. And we're stuck with that. Another issue, it's super important to prioritize the development. Going chaotic, implementing random features, and this happens if you start merging random PRs. It's really bad. It doesn't really scale. I think prioritization is super important. And this model where you keep merging random PRs does not work. This is a strong belief I have.
So you're a depth-first search kind of guy. And when you build something successful that involves lots of other people, you have to become more like breadth-first search. And because there are so many things that are coming in every single day. And I remember there was a bit in Kevin's book where he said, at some point, you just kicked a load of people off the Slack channel and you said, look, I just need to, I just need to focus there because it was getting ridiculous.
Yes. Oh, yes. Yeah. I forgot about this story of the kicking. Yeah, because at the point, at that point, wow, I really dislike people that keep throwing ideas. I mean, they don't even. They're having fun. I mean, it's different. I mean, for me, I was trying to build something that works. Some people were there in the Slack channel having fun, throwing ideas on the wall, right? I mean, it's cheap. I mean, you can throw ideas on the wall and the other side has. To keep telling your noise, this doesn't work. Something that's for me, one frustrating scenario. You throw an idea. You didn't spend five minutes thinking about it. Then I find a hole. I send back to you. Then you polish a little bit, send back. Now it takes 10 minutes to find the hole, the next hole. It keeps taking exponentially longer to find the holes on the FBAK idea. For the person coming up with them, it's fun, I mean, but it's not fun from your receiver, right? You have to do your work now. You spend time telling people why this is not a good idea, why it's not the time to do it. Yeah, there was a point. Yes, I kicked out. I mean, stage only the core team that was really contributing to the project. Only people that were writing useful code to the project stage.
Yeah, it must be even worse now with Generative AI. I mean, so what you're pointing to there, it's called Brandellini's Law, which is that it takes exponentially more work to debunk bullshit than create it.