*To*: <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] lexical matters*From*: <mark at proof-technologies.com>*Date*: Wed, 19 Jan 2011 02:50:20 +0000*Reply-to*: mark at proof-technologies.com

on 18/1/11 10:22 PM, Gerwin Klein <gerwin.klein at nicta.com.au> wrote: >> We should remember that at the moment it is very easy for someone to >> maliciously produce what appears to be a formal proof of some statement >> ... > > I don't think this is a problem in practice. Theorem provers are already > used in big certification projects. The evaluators in such projects usually > know what they are doing, How can you be so confident about this? In the large, safety-critical certification projects I have been involved with, the evaluators do the best they can with the tools they have available. Proof checkers with readable and highly trustworthy output is a luxury not available to them. > at least up to the level where they would easily > be able to spot attempts to make syntactically misleading proof statements. > It's easy enough to scan for ML blocks or similar in theory files, spot > duplicate identifiers, etc, and demand good explanations for their presence > (or just forbid them). And the threat of just using a proof checker is > always there, so why try to cheat on syntax? The input in this process is the full power of an ML program. We all know that it is possible to hide incredibly subtle things in huge programs. Are we to ban non-trivial ML in the process of producing a proof? This would be forcing contractors to do their work with one hand tied behind their back. The contracted, safety-critical proof work I have been involved with would certainly have been completely infeasible without writing large amounts of ML program to support my proof work. It is far better for the auditor if they can treat the ML code that establishes the final theorem as some sort of black box. To do this the theorem prover needs certain basic properties, including a trustworthy printer. > I'm with Larry on this: the much bigger problem is to convince yourself that > the model and final theorem are in any way useful or right. This is where > cheating will happen much earlier. I did not say that this was not a problem! This is the big problem! And this is the problem that I am advocating needs a tool that properly supports the process - the process of determining that the model and final theorem are right (as well as that the final theorem has actually been proved). This process involves using the pretty printer. Mark.

**Follow-Ups**:**Re: [isabelle] lexical matters***From:*Gerwin Klein

- Previous by Date: Re: [isabelle] lexical matters
- Next by Date: Re: [isabelle] lexical matters
- Previous by Thread: Re: [isabelle] lexical matters
- Next by Thread: Re: [isabelle] lexical matters
- Cl-isabelle-users January 2011 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list