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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
