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
This archive was generated by a fusion of
Pipermail (Mailman edition) and