[isabelle-dev] auto raises a TYPE exception

[Tobias Nipkow]

I am not saying we shouldn't prove bits of the code. By all means, do it. But
until you have verified the whole kernel, it just increases some warm feeling we
have about the code. In this particular case, verification would not have helped
that much because the problem came from the violation of an unstated
precondition. So in addition to verifying the unification code you have to
verify all calls of it.

Assertions/testing and verification are complementary, with very different costs
and benefits.

Tobias


Am 30/05/2013 11:50, schrieb Makarius:
> On Thu, 30 May 2013, Tobias Nipkow wrote:
> 
>> this incident has again reminded me that in the absence of formal proofs about
>> the code, assertions in the code would be a big step forward. they could have
>> told us a long time ago that some precondition expected by the unification
>> code is not guaranteed.
> 
> Concerning "the code", it really just refers to these two special modules:
> pattern.ML and unify.ML.  All the rest has gradually been improved over 20
> years, so that it does not suffer from any such uncertainty.  (Otherwise the
> system would still be the tiny research experiment that it used to be in the
> 1980-ies, not the big thing we have today.)
> 
> 
>> lukas and a student had even put together a quickcheck infrastructure for
>> Isabelle/ML. All of this could be confined to regression runs. i think we
>> should make some effort in this direction to increase our confidence in the
>> kernel.
> 
> When Lucas Buhlwahn started this experiment, I pointed him to pattern.ML and
> unify.ML as the key problem zones.  At the same time it was clear that a little
> proof-of-concept with quickcheck cannot address the more profound questions that
> arise here.
> 
> For these particular modules, I would like to see a proper formalization of what
> it really is.  The question of how schematic polymorphism conceptully interacts
> with HO unification does not seem to be resolved after such a long time.
> 
> 
>     Makarius