Re: [isabelle] lexical matters



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.

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.