Comment by raincole

> should not the chance of bugs be about equal in both of them?

Why?

Are you saying that all the programs ever written have the exact same chance of bugs? A hello world is as buggy as a vibe-coded Chromium clone?

If you accept the premise that different programs have different chances to have bugs, then I'd say:

1. Simpler programs are likely less buggy.

2. Programs used by more people are likely less buggy.

3. Programs maintained by experts who care about correctness are likely less buggy.

4. Programs where the stakes are higher are likely less buggy.

All things considered, I think it's fair to say Lean is likely less buggy then a random program written by me at weekend.

> Heisenberg's uncertainty theorem

It has nothing to do with the uncertainty principle. If you think otherwise, it means your understanding of uncertainty principle comes from sci-fi :)