Re: [isabelle] lexical matters



on 18/1/11 12:38 PM, Lawrence Paulson <lp15 at cam.ac.uk> wrote:

> Obviously trustworthiness is important. Nevertheless, a fixation on this
one
> issue can be counter-productive. I'm not aware of a single piece of
research
> that was invalidated due to bugs in theorem provers. On the other hand, I
> have seen a great many papers where the work was essentially worthless
> because of inadequate modelling of the problem. Naturally, the theorem
> prover cannot check that a model is realistic, but I frequently hear the
> suggestion that nothing can go wrong if you use a theorem prover. The
> community needs to focus more on ways of making models trustworthy. There
> are probably quite a few interesting research topics along those lines.

I agree that there are more important issues that require more attention.
I'm not advocating endless fixation with cosmic rays and the like, but just
a healthy degree of concern, especially when the problems can be easily
addressed.

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 but
is in fact something that takes advantage of the sorts of pretty printer
problems I am talking about.  Now if theorem provers are ever going to make
it big, we are then in the situation where commercial pressures, etc, are
pushing people to claim they have proved something when they have in fact
not.  One of the important roles of a theorem prover should be as a highly
trustworthy tool to support a human proof auditor checking that some huge
10,000 line proof of a theorem does indeed establish the theorem.

Mark.

>
> Larry Paulson
>
> On 18 Jan 2011, at 11:55, <mark at proof-technologies.com> wrote:
>
>> on 17/1/11 11:14 PM, Makarius <makarius at sketis.net> wrote:
>>
>>> There are other, more pressing problems.
>>
>> I think trustworthiness in theorem provers should always be a top
> priority.
>> After all, this is why we are using them in the first place.  So long as
> it
>> doesn't have terrible consequences on other aspects of the theorem
prover,
>> such as efficiency or usability, that is.
>
>
>
>





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