[isabelle-dev] auto raises a TYPE exception

[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