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