Email Gateway (Aug 22 2022 at 14:51): Email Gateway (Aug 22 2022 at 14:51):From: Makarius <makarius@sketis.net>
Reading the sources, reading papers, asking people who should know how
these systems are done, listening carefully. I do that myself when
talking to the colleagues behind the other systems (HOL4, HOL-Light,
Coq, ACL2, ProofPower).
The assumption that any of the LCF-style provers is 100% correct is
wrong -- that was never the case in last decades. If your work depends
on that assumption, you need to rethink what you are doing.
We need more clarity and more honesty.
Makarius
Email Gateway (Aug 22 2022 at 14:51):From: Makarius <makarius@sketis.net>
Here is actually an opportunity to listen (in German):
https://www.youtube.com/watch?v=R8pyFwil9KY from minute 27:32 -- a
question in the off about HOL-Light's "kleiner Kern" that leads to an
abstract explanation about prover (in)correctness by myself.
Makarius
Email Gateway (Aug 22 2022 at 14:51):From: Makarius <makarius@sketis.net>
Hugo Herbelin is actually an expert an that.
Here is an example from a recent thread on coq-club "safe interface for
writing Coq plugins"
https://sympa.inria.fr/sympa/arc/coq-club/2016-11/msg00080.html (a
"plugin" is just an OCaml module produced by the user; in Isabelle/ML
that is trivial and does not need a special name).
That is an accurate and calm explanation of the realities of Coq,
without causing an uproar on the mailing list. Very professional.
Makarius
Email Gateway (Aug 22 2022 at 14:51):From: Randy Pollack <rpollack@inf.ed.ac.uk>
Absolute certainty cannot be obtained by millions of lines of code
(prover, compiler, OS, ...) running on real hardware, but, as Hugo
points out, independent checking goes some ways toward improved
confidence.
Truly independent checking is asking a lot of a reader of a formal
development, but Coq has stand-alone
coqchk; some HOLs can be checked by HOL-zero.
What is the story for stand-alone checking of Isabelle/Hol developments?
Email Gateway (Aug 22 2022 at 14:52):From: Makarius <makarius@sketis.net>
I keep asking that same question whenever I meet people who have to
potential to do it, e.g. the CakeML guys.
Ultimately I would like to see:
(1) A common understanding of HOL as a logic, by all providers of some
HOL variant.
(2) An independent programming language implementation (other than
Poly/ML). E.g. verified CakeML or something totally different (verified
Rust?); better not C++ or OCaml.
(3) An independently implemented and maintained HOL proof checker
based on (1) and (2).
As a start, one could target at a proper Isabelle/HOL ~> OpenTheory
export tool. (It will also require some reforms in Isabelle to make it
really fit.)
Makarius
Email Gateway (Aug 22 2022 at 14:52):From: Lawrence Paulson <lp15@cam.ac.uk>
There is a totally different way of looking at correctness. It doesn’t replace technical means (proof kernels, separate checkers), but complements them. It is to make the proof readable to humans as well as to machines, so that a particular proof can be can be inspected by a mathematician using no tools but the human eye.
From the point of view of many mathematicians, reliance on computers introduces too much uncertainty. They worry not only about subtle bugs in the code (even if confined to a kernel of a few hundred lines) but about cosmic rays and the like. I find this point of view extreme, but it is there. With such a point of view, even a fully bootstrapped verification of the prover implementation on a verified compiler may be suspect, because the proof itself will look to such a sceptic as nothing but thousands and thousands of lines of additional code.
Here the legibility of the proof itself offers a different type of confidence. If the premises and conclusion of the theorem are clear, and the correctness of each step (shown by explicit intermediate assertions, for example using “have”) can be verified by inspection, then a mathematician can be convinced by such a proof independently of what may be going on in the machine. It is of course possible that the mathematician’s interpretation of the proof (and even the formal language it was written in) might deviate from the intended meaning.
Larry Paulson
Email Gateway (Aug 22 2022 at 14:52):From: Mark Adams <mark@proof-technologies.com>
This is good if the proof scripts are readable and can then be read over
by mathematicians for added assurance. But it doesn't really help in
cases where the formal proof uses highly automated steps, like in much
of Flyspeck, especially in the parts of Flyspeck where linear and
non-linear inequalities are dealt with.
Mark.
Email Gateway (Aug 22 2022 at 14:53):From: Tobias Nipkow <nipkow@in.tum.de>
On 12/12/2016 00:19, Randy Pollack wrote:
Absolute certainty cannot be obtained by millions of lines of code
(prover, compiler, OS, ...) running on real hardware, but, as Hugo
points out, independent checking goes some ways toward improved
confidence.Truly independent checking is asking a lot of a reader of a formal
development, but Coq has stand-alone
coqchk; some HOLs can be checked by HOL-zero.What is the story for stand-alone checking of Isabelle/Hol developments?
There are proof terms in Isabelle/HOL, but they share a lot of the
infrastructure with the rest of the system. In this example, however, they do
the right thing: calling Proof_Checker.thm_of_proof with the proof term for the
circular proof fails.
Tobias
On Sun, Dec 11, 2016 at 10:48 PM, Makarius <makarius@sketis.net> wrote:
On 11/12/16 23:17, Makarius wrote:
We need more clarity and more honesty.
Hugo Herbelin is actually an expert an that.
Here is an example from a recent thread on coq-club "safe interface for
writing Coq plugins"
https://sympa.inria.fr/sympa/arc/coq-club/2016-11/msg00080.html (a
"plugin" is just an OCaml module produced by the user; in Isabelle/ML
that is trivial and does not need a special name).That is an accurate and calm explanation of the realities of Coq,
without causing an uproar on the mailing list. Very professional.Makarius
Last updated: Apr 19 2024 at 20:15 UTC