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

On Apr 29, 2010, at 2:17 PM, Tobias Nipkow wrote:

> We have to distinguish two applications of proof objects: to speed up
> the loading of theories, where they are fine, 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...

Actually I have been thinking about these kinds of problems for a while. IMHO,
you can choose between two options here:

a) Do it how Isabelle (and the AFP) does it currently: When the Isabelle system
changes, change all proofs and theorems and so on to become up-to-date.

b) Develop a versioning system that not only manages source code (like it is
currently done) but also content (theories, theorems, proofs, and so on). Part
of this versioning system is also a mechanism on how to transfer content from
one version to another (most of the time nothing has to be done here; for
example for a minimal implementation of such a versioning system there is most
of the time no need to transfer proofs, but only theorems). And yes, this means
that at least a part of the versioning system becomes part of the trusted kernel
of the proof assistant.

I think of those two options only option b) scales to hundreds of thousands of
concurrent users. A working versioning system like proposed in b) does not
exclude a): You can still do refactoring, to use newer proof methods for
example. But you don't have to.

By the way, can anyone here provide pointers to previous work that goes in the
direction of b) ?

- Steven

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