[isabelle-dev] Fwd: A possible bug with Isabelle 2013

[Lawrence Paulson]

I don't think it's helpful to argue about terminology. Many problems have deep and complicated causes, as in the case of the Ariane 5 launch failure. They aren't just simple coding errors, and using the word "fixed" does not imply that carelessness is to blame. But I do think that a simple solution is possible in this situation (calculations). To me it hardly differs from "Fails to refine any pending goal", and it should be treated similarly.

Larry

On 27 Feb 2013, at 14:28, Makarius <makarius at sketis.net> wrote:

> On Wed, 27 Feb 2013, Lawrence Paulson wrote:
> 
>> A behaviour where "..." denotes something other than the previous right-hand side needs to be fixed.
> 
> Again this odd "bug -- fixed" terminology. Such problems are much deeper.
> 
> Fortunately, the solution for overly polymorphic results, and the extreme form of so-called hidden-polymorphism, has been mostly there for several years.  We had really big structural problems in the past, but this is now forgotten.
> 
> What is missing is some immediate visual feedback about what the system has produced from user input.  This applies to plain Hindley-Milner generalization, implicit itself arguments, and coercions.
> 
> Note that in mainstream programming communities, even just Hindley-Milner without anything in addition is often found in the "type-inference sucks" corner of discussion forums.
> 
> 
> 	Makarius