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



Thanks all, I think this has been a productive discussion :)

I would like to respond to a point Makarius brought up earlier:

On 07/07/17 18:37, scott constable wrote:
>
> possibly written by other persons with malicious intentions.

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.

I'm also familiar with Coq, and I do think Coq should be better in this
respect. In Coq, proofs are themselves objects with a given type. So they
can be checked or examined, for instance by dumping them to the console. So
to check the legitimacy of a theorem in Coq, I believe it would suffice to
walk the proof tree by recursively expanding each non-atomic node, and thus
ensure that the proof tree is composed entirely of legitimate proof objects.

Am I wrong about this? If not, might there be a similar approach in
Isabelle?

Scott



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