Re: [isabelle] Proof by analogy and proof stability in Isabelle
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and