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



Scott,

Of course you are right and if some prover does not guarantee correctness on its own, that is the standard answer: proof terms. Isabelle has had proof terms for a long time now, but their checker is also part of Isabelle and uses the same infrastructure of terms, types etc. Hence it is only as reliable as that infrastructure is. An independent checker would improve the situation. That's why, for example, for SAT solvers independent and verified proof checkers are becoming available.

The discussion about "malicious intentions" never ceases to amaze me. Using the interfaces that a system offers is not malicious by definition of the term interface. If it requires wizard status to know what is ok and what not, that is a design decision one can take, but then one need not be suprised that non-wizards may perceive this as risky.

Appealing to readable proofs is not a panacea as Mark Adams' email shows: the proofs about the linear inequalities he refers to are by necessity machine generated and beyond human checking. But we would still like to have strong correctness guarantees.

Tobias

On 08/07/2017 19:12, scott constable wrote:
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


Attachment: smime.p7s
Description: S/MIME Cryptographic Signature



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