4 ms·

Your analogy to buggy implementations in ordinary programming languages is deeply flawed though. The things formally defined and stated are proven. There can b

Your analogy to buggy implementations in ordinary programming languages is deeply flawed though. The things formally defined and stated are proven. There can be no bugs in a library that lead to formally stated theorems being erroneously proven. Bugs at the library level can only appear in the form that formally stated theorems might not be what you think they are. So I object to your characterization that they might be mathematically incorrect. The mathematical content might be different than believed though.

bmitc 2y ago
> The things formally defined and stated are proven. There can be no bugs in a library that lead to formally stated theorems being erroneously proven. That can't actually be true in practice can it? These are things running on a computer, a machine, and not paper. Additionally, I'm consider two types of "bugs". (1) bugs in software or hardware that the stack relies on; (2) "bugs" in the conceptual sense of a Lean construction being something different than what was meant or what people thought it was, which is effectively the same problem that regular mathematics runs into.
- naasking 2y ago
  > Additionally, I'm consider two types of "bugs". (1) bugs in software or hardware that the stack relies on; Then run the Lean proof on a non-x86 computer and on both Windows and Linux. The possibility that two independent computer architectures and two independent operating systems converge on some buggy behaviour that just so happens to allow a buggy proof through is so remote it's not worth considering further. > (2) "bugs" in the conceptual sense of a Lean construction being something different than what was meant or what people thought it was, which is effectively the same problem that regular mathematics runs into. A specification is orders of magnitude shorter than proofs, on average. So if you're saying they managed to reduce the amount of manual verification work and possible human error by orders of magnitude, that sounds like an uncontroversial win for correctness.
- Certhas 2y ago
  Theorem provers work like this: the axioms are input, then there is a program (using libraries) that transforms them, and the output of that program is the theorem. If the runtime is correctly executing the program, then the theorem is proven from the axioms. Importantly, as long as there is any program that outputs the theorem from the axioms, you have a proof. So even if your program doesn't do what you think it does, if it outputs the theorem, that doesn't matter. So do you trust the runtime? Bit flip errors can be eliminated by running things multiple times. The more human proven statements the runtime executes correctly the more you believe it's implemented correctly. Importantly, all proofs done in lean increase the trust in the common runtime. And: do you trust your ability to understand the formal theorem that is output. That's the question discussed elsewhere in this comment section in depth.
- epgui 2y ago
  > That can't actually be true in practice can it? These are things running on a computer, a machine, and not paper. It's true for all practical purposes. Humans are just running on protein, lipids and sugars, and these are far less reliable than transistors.

bmitc 2y ago

> The things formally defined and stated are proven. There can be no bugs in a library that lead to formally stated theorems being erroneously proven. That can't actually be true in practice can it? These are things running on a computer, a machine, and not paper. Additionally, I'm consider two types of "bugs". (1) bugs in software or hardware that the stack relies on; (2) "bugs" in the conceptual sense of a Lean construction being something different than what was meant or what people thought it was, which is effectively the same problem that regular mathematics runs into.

naasking 2y ago
> Additionally, I'm consider two types of "bugs". (1) bugs in software or hardware that the stack relies on; Then run the Lean proof on a non-x86 computer and on both Windows and Linux. The possibility that two independent computer architectures and two independent operating systems converge on some buggy behaviour that just so happens to allow a buggy proof through is so remote it's not worth considering further. > (2) "bugs" in the conceptual sense of a Lean construction being something different than what was meant or what people thought it was, which is effectively the same problem that regular mathematics runs into. A specification is orders of magnitude shorter than proofs, on average. So if you're saying they managed to reduce the amount of manual verification work and possible human error by orders of magnitude, that sounds like an uncontroversial win for correctness.
Certhas 2y ago
Theorem provers work like this: the axioms are input, then there is a program (using libraries) that transforms them, and the output of that program is the theorem. If the runtime is correctly executing the program, then the theorem is proven from the axioms. Importantly, as long as there is any program that outputs the theorem from the axioms, you have a proof. So even if your program doesn't do what you think it does, if it outputs the theorem, that doesn't matter. So do you trust the runtime? Bit flip errors can be eliminated by running things multiple times. The more human proven statements the runtime executes correctly the more you believe it's implemented correctly. Importantly, all proofs done in lean increase the trust in the common runtime. And: do you trust your ability to understand the formal theorem that is output. That's the question discussed elsewhere in this comment section in depth.
epgui 2y ago
> That can't actually be true in practice can it? These are things running on a computer, a machine, and not paper. It's true for all practical purposes. Humans are just running on protein, lipids and sugars, and these are far less reliable than transistors.