3 ms·
The issue is not the edge of logical independence, but rather how easily can you express certain theorems. Most verification is about the verification of progra
by mafribe 9y ago
The issue is not the edge of logical independence, but rather how easily can you express certain theorems. Most verification is about the verification of programming languages (e.g. the POPLmark Challenge [1]), and in this setting sometimes what you want to prove is more convenient to express in the CoC. You can also express it in HOL, but not quite as easily.
All that said, automation of provers based on the LCF approach with a non-constructive logic is much superior as of December 2017. With this in mind I was surprised to see that L. de Moura based the new Lean prover [2] on a variant of the CoC. He thinks that all automation that we currently have for HOL (i.e. Isabelle/HOL) can be brought to Lean.
J. Blanchette [3] seems to think the same.
[1] https://www.seas.upenn.edu/~plclub/poplmark https://www.seas.upenn.edu/~plclub/poplmark
[2] https://leanprover.github.io https://leanprover.github.io
[3] https://people.mpi-inf.mpg.de/~jblanche https://people.mpi-inf.mpg.de/~jblanche
- wizeman 9y ago> sometimes what you want to prove is more convenient to express in the CoC. You can also express it in HOL, but not quite as easily. > All that said, automation of provers based on the LCF approach with a non-constructive logic is much superior as of December 2017. This is kind of the point I am making. Is the fact that some things are more convenient to express worth the substantial loss of automation? > With this in mind I was surprised to see that L. de Moura based the new Lean prover [2] on a variant of the CoC. He thinks that all automation that we currently have for HOL (i.e. Isabelle/HOL) can be brought to Lean. > J. Blanchette [3] seems to think the same. Interesting, thanks! I hope they are right and in the future this kind of automation does come to Coq and Lean.