Re: [isabelle] Verify the legitimacy of a proof?
I think that we are talking at cross purposes here. Of course we want our systems to be sound, and a kernel architecture is a great help in this, as we have known for 40 years. But even with a kernel architecture, it is easy for a result to be misrepresented. See e.g.
> Avra Cohn. The Notion of Proof in Hardware Verification. J. Autom. Reasoning5(2): 127-139 (1989)
The proof kernel is no defence whatever against misrepresentation or misunderstanding, so itâs important that formal documents are openly available for inspection.
> On 10 Jul 2017, at 10:10, Peter Lammich <lammich at in.tum.de> wrote:
> On Sa, 2017-07-08 at 19:59 +0100, Lawrence Paulson wrote:
>> "We have been given a proof of X; Is it credible?"
> At this point, I second Ken. Although having human-readable machine
> checked proofs is certainly a nice feature to get an idea of how a
> proof works, the main points to check should be the statement of the
> theorem, including the definitions (syntax tweaks, etc) it uses, as
> well as the axioms its proof uses. Then, one relies on the logical
> inference kernel that the proof is actually correct.
> In particular, auxiliary lemmas and definitions only used for the
> proof, but not in the main statement of the theorem, should be
> irrelevant for trusting the theorem.
> This principle should, in first place, be independent of whether the
> user is malicious or not. However, in Isabelle, the malicious user has
> a lot of possibilities to hide tweaks from a reviewer, while, in
> HOLZero, these possibilities are very limited (if existent at all).
> Actually, Isabelle contains many tools in this spirit, for example,
> even the simplifier or classical reasoner apply some transformations on
> the theorems provided to them. More high-level tools like function
> package or datatype package even do really complex proofs, completely
> hidden from the user.
This archive was generated by a fusion of
Pipermail (Mailman edition) and