*To*: <cl-isabelle-users at lists.cam.ac.uk>*Subject*: Re: [isabelle] lexical matters*From*: <mark at proof-technologies.com>*Date*: Tue, 18 Jan 2011 13:01:59 +0000*Reply-to*: mark at proof-technologies.com

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. > > > >

**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