Re: [isabelle] Verify the legitimacy of a proof?



On 08/07/17 15:33, Tobias Nipkow wrote:
> 
> On 08/07/2017 13:30, Makarius wrote:
>> On 08/07/17 13:01, Manuel Eberl wrote:
>>> Unfortunately, it is very easy to circumvent this. I don't recall who
>>> found this originally, but you can hide the âtaintâ of a theorem by
>>> going through a type class instantiation:
>>
>> "Found this originally" sounds very funny to me.
>>
>> Of course, the problem of oracles vs. type classes instantiations is as
>> old as oracles and type class instantiations in Isabelle. It is rather
>> well-known for insiders.
> 
> I am sure Manuel meant no disrespect. No doubt you were aware of this
> behaviour from the start.

No, and neither did I mean any disrespect to Manuel.


>> So we are back to the new meta-problem from recent years: even power
>> users don't know anymore what Isabelle is and what it does, and
>> especially what it does not.
> It is usually due to a fanciful interpretation of the documentation. The
> latter says that "The system always records oracle invocations within
> derivations of theorems by a unique tag." but does not claim that these
> tags are also always inherited in the way one is all too likely to
> assume.

The problem remains open: How can true expertise about how Isabelle
really works be reconstructed? We've seen a slow and steady decline in
the past 10 years, and myself writing hundreds of pages of documentation
helped only very little.


	Makarius





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