Re: [isabelle] Type definitions in Isabelle; article "A Consistent Foundation for Isabelle/HOL" by KunÄar/Popescu

How about III,
a user devised a definition that is meaningful but mistakenly omits a word (eg "primrec") somewhere, and could "complete his project" or so it seems, by virtue of the fact that his definitions are nonsense, but not obviously so


On 23/08/16 20:31, Lawrence Paulson wrote:
On 23 Aug 2016, at 01:38, Andrei Popescu <A.Popescu at> wrote:

So what are we talking about here?

We are talking about the danger â almost certainly realised â of misleading people.

The various issues involving Isabelle, Coq, PVS and other systems are all complicated in their details. Outside observes are probably not going to invest the time and effort necessary to investigate precisely what is going on in case case. They will regard these âinconsistenciesâ as roughly the same. So we are drawing a false equivalence between

I. The prover incorrectly handles correct and meaningful definitions. Users, who have done nothing wrong, cannot complete their projects.

II. Somebody who has studied the source code has devised a definition that is not meaningful and the prover fails to detect this. Nobody has ever used or wanted such a definition, because it is overtly nonsensical.

Itâs wrong and misleading to give the impression that I and II are the same.


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