4 ms·

However, prover[p-1] can prove prover[p], modulo the bugs prover[p-1]. Then prover[p-2] can prove prover[p-1], modulo the bugs in prover[p-2]. If you can have

However, prover[p-1] can prove prover[p], modulo the bugs prover[p-1]. Then prover[p-2] can prove prover[p-1], modulo the bugs in prover[p-2]. If you can have prover[i-1] is simplier than prover[i], and prover[0] is so simple that any 5-years old can prove it's correct, then you win.

randallsquared 10y ago
Something seems wrong about this. Could you not describe the combination of all provers as a formal system? Would this system then not run afoul of Goedel?
- deleted 10y ago
  [deleted]
- lmkg 10y ago
  This approach can only describe formal systems that are finite combinations of such provers.
- crpatino 10y ago
  Theoretically, you are 100% correct. In practice, it is still worthwhile to have N redundant independently developed provers to prove each other, and to benchmark against each other. This will help uncover subtle bugs that result from ordinary programming mistakes. This will, however, not protect against deeper issues that are common to all N provers. e.g. Potential biases or mistaken assumptions in the formal verification comunity. At the end of the day, it is an engineering decision. How much of the available resources are you willing to through at the practical problem of making your implementation approach asymptotically to the theoretical limits. The fact that those limits is indeed a peg or two below perfection is an independent issue.
  - nickpsecurity 10y ago
    "In practice, it is still worthwhile to have N redundant independently developed provers to prove each other, and to benchmark against each other. This will help uncover subtle bugs that result from ordinary programming mistakes." I strongly advise that to deal with both mistakes and subversion. Mutually-suspicious parties in various countries using different logics, compilers, hardware, etc. with a common, executable spec that's basically state machines or functions. That way they get same output from same input. So, when I saw Milawa was verified first-order, I immediately looked for other verifications of first-order provers (found 1). Then the idea would be diverse implementations of executable parts of that stack with diverse reviews of logic combinations they did. Exhaustive testing done by each party. Even do implementations of key parts of TCB in other logics to check results. The prover with its code is trustworthy when everyone got the same results on same logics, code, shared tests, and individual tests. Plus have paper copies of the resulting text files with hashes stashed away somewhere in case a nation-state wants to throw money at countering diversity via hacking host systems. ;) Then we rinse and repeat for more complex provers. The fun never stops in this game.
- vilhelm_s 10y ago
  The end result you get out is something like "if the prover n accepts the claim P, then prover 1 also accepts the claim P". In logical terms you can think of it as a relative consistency proof. In practice, even much simpler theorems would already raise our confidence a lot. E.g., the inference rules of Coq can be stated in a couple of pages of text, but the kernel checker that you need to trust is 14k lines of OCaml. A proof that the checker actually correctly implements the inference rules would already catch the majority of the bugs that happen in practice. Because of Gödel we then can't hope for a proof in Coq that there is no way to use those inference rules to derive False, but that's less of a concern.
JadeNB 10y ago
> prover[0] is so simple that any 5-years old can prove it's correct This seems like the perfect time to misquote Groucho Marx: "This is so simple a child of 5 could prove it. Somebody bring me a child of 5!"
nickpsecurity 10y ago
Good thinking. That's exactly how they did it: https://news.ycombinator.com/item?id=12762224 https://news.ycombinator.com/item?id=12762224

randallsquared 10y ago

Something seems wrong about this. Could you not describe the combination of all provers as a formal system? Would this system then not run afoul of Goedel?

deleted 10y ago
[deleted]
lmkg 10y ago
This approach can only describe formal systems that are finite combinations of such provers.
crpatino 10y ago
Theoretically, you are 100% correct. In practice, it is still worthwhile to have N redundant independently developed provers to prove each other, and to benchmark against each other. This will help uncover subtle bugs that result from ordinary programming mistakes. This will, however, not protect against deeper issues that are common to all N provers. e.g. Potential biases or mistaken assumptions in the formal verification comunity. At the end of the day, it is an engineering decision. How much of the available resources are you willing to through at the practical problem of making your implementation approach asymptotically to the theoretical limits. The fact that those limits is indeed a peg or two below perfection is an independent issue.
- nickpsecurity 10y ago
  "In practice, it is still worthwhile to have N redundant independently developed provers to prove each other, and to benchmark against each other. This will help uncover subtle bugs that result from ordinary programming mistakes." I strongly advise that to deal with both mistakes and subversion. Mutually-suspicious parties in various countries using different logics, compilers, hardware, etc. with a common, executable spec that's basically state machines or functions. That way they get same output from same input. So, when I saw Milawa was verified first-order, I immediately looked for other verifications of first-order provers (found 1). Then the idea would be diverse implementations of executable parts of that stack with diverse reviews of logic combinations they did. Exhaustive testing done by each party. Even do implementations of key parts of TCB in other logics to check results. The prover with its code is trustworthy when everyone got the same results on same logics, code, shared tests, and individual tests. Plus have paper copies of the resulting text files with hashes stashed away somewhere in case a nation-state wants to throw money at countering diversity via hacking host systems. ;) Then we rinse and repeat for more complex provers. The fun never stops in this game.
vilhelm_s 10y ago
The end result you get out is something like "if the prover n accepts the claim P, then prover 1 also accepts the claim P". In logical terms you can think of it as a relative consistency proof. In practice, even much simpler theorems would already raise our confidence a lot. E.g., the inference rules of Coq can be stated in a couple of pages of text, but the kernel checker that you need to trust is 14k lines of OCaml. A proof that the checker actually correctly implements the inference rules would already catch the majority of the bugs that happen in practice. Because of Gödel we then can't hope for a proof in Coq that there is no way to use those inference rules to derive False, but that's less of a concern.

JadeNB 10y ago

> prover[0] is so simple that any 5-years old can prove it's correct This seems like the perfect time to misquote Groucho Marx: "This is so simple a child of 5 could prove it. Somebody bring me a child of 5!"

nickpsecurity 10y ago

Good thinking. That's exactly how they did it: https://news.ycombinator.com/item?id=12762224 https://news.ycombinator.com/item?id=12762224