Re: [isabelle] Proof by analogy and proof stability in Isabelle



Proof stability is an interesting topic to discuss, but the tenor of the discussion may give a misleading impression. Proof stability is chiefly an issue for the Isabelle developers. We have over 600,000 lines of proof scripts to maintain, about half in Isabelle/HOL and half in the AFP. Many of these proof scripts are over 10 years old and refer to numerous deprecated features. They can be a nightmare to maintain.

I would be surprised if proof stability was the leading issue with users. I certainly do not recall losing much time in the course of a proof development to patching up failing proofs, even though (unlike most ordinary users surely) I invariably use potentially unstable development snapshots. The simplest way to achieve proof stability, as advocated particularly by some Coq users, is to avoid automation altogether. The problem with that approach is that it takes much longer to prove anything.

Larry Paulson


On 30 Apr 2010, at 01:59, Tjark Weber wrote:

> On Thu, 2010-04-29 at 14:17 +0200, Tobias Nipkow wrote:
>> We have to distinguish two applications of proof objects: to speed up
>> the loading of theories, where they are fine,
> 
> If I recall correctly, Makarius and Stefan conducted a few experiments
> some years ago and concluded that checking proof objects was typically
> not faster than re-playing proof scripts in Isabelle.
> 
>> and as a means of
>> producing stable proofs, where I maintain they are problematic (and I am
>> not aware of any system that supports it). If you want to protect your
>> proof against a changing basis, you have to include the whole basis into
>> your proof object. It is not infeasible, but it means you are locked
>> into this one version of your proofs. And if one day the format for
>> primitive proofs changes...
> 
> Well, being locked into a particular version of Isabelle's proof checker
> still seems much better than being locked into a particular version of
> Isabelle (and worse, being locked into a particular system configuration
> when external provers are used).
> 
> Of course proof objects are not the answer to life, the universe and
> everything.  Size is one issue; the lack of readability is another.  But
> in terms of stability across Isabelle versions and platforms, proof
> objects beat proof scripts (and even well-written Isar proofs) by a wide
> margin.  The interface is just a lot simpler.
> 
>> It is like packaging every library your
>> program needs with that program (in binary) and freezing the program at
>> that point. It may have its uses, but it is not recommended as a general
>> program development method.
> 
> Proof objects can refer to lemmas, so one isn't forced to freeze the
> library.  Of course changes to the library may cause proof checking to
> fail then, but at least changes to tactics still won't.
> 
> Shipping libraries in binary form is actually quite common, isn't it?
> Maybe we need an equivalent for Isabelle theories.
> 
> Tjark
> 
> 






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.