Re: [isabelle] lexical matters



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.





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