[isabelle-dev] auto raises a TYPE exception

[Lawrence Paulson]

There might be a lot of interesting projects that involve verifying parts of our code, and any of these could be beneficial, even if only parts of the code are covered. I guess it would be in the spirit of the recent trend to studying the semantics of real things. The only question is whether Isabelle is important enough for such work to be seen as significant in a wider context. But certainly such work would be good enough to get an MPhil.
Larry

On 30 May 2013, at 12:13, Tobias Nipkow <nipkow at in.tum.de> wrote:

> 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
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev