Re: [isabelle] Verify the legitimacy of a proof?

To protect against malicious intentions would turn Isabelle into a form of security software. But the guarantees we get from the latter are quite different from what we get from a formal proof. Ultimately security claims depend upon trusting a lot of complicated mechanisms, such as certificate authorities and cryptosystems. We are not a lot better off than when a model checker comes back with nothing.

However, we work with formal proofs, which can be examined, even interactively. We do not have to work on the basis that "X has been proved, therefore X is true", but rather "We have been given a proof of X; Is it credible?" Then we can look at any part of this proof where we have doubts. A devious user has many ways to try to fool us, but it's not so easy if he has to supply the full source code and we insist on legibility throughout. The effort we choose to invest in this would depend on how important X is and how much we distrust the person who supplied the proof.

Larry Paulson

> On 8 Jul 2017, at 18:12, scott constable <sdconsta at> wrote:
> Isabelle does not protect against malicious intentions. It would require
> a quite different system to do that, one that you won't like to use.
> The other big provers (e.g. Coq) are similar in this respect.

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.