*To*: isabelle-users at cl.cam.ac.uk*Subject*: Re: [isabelle] Proof by analogy and proof stability in Isabelle*From*: "steven at obua.de" <steven at obua.de>*Date*: Thu, 29 Apr 2010 14:46:32 +0200 (CEST)*In-reply-to*: <4BD978ED.2000106@in.tum.de>*References*: <6031272389962@web71.yandex.ru> <4BD91699.8020401@in.tum.de> <1272538820.2300.49.camel@weber> <4BD978ED.2000106@in.tum.de>

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

**Follow-Ups**:**Re: [isabelle] Proof by analogy and proof stability in Isabelle***From:*Brian Huffman

**References**:**[isabelle] Proof by analogy and proof stability in Isabelle***From:*grechukbogdan

**Re: [isabelle] Proof by analogy and proof stability in Isabelle***From:*Tobias Nipkow

**Re: [isabelle] Proof by analogy and proof stability in Isabelle***From:*Tjark Weber

**Re: [isabelle] Proof by analogy and proof stability in Isabelle***From:*Tobias Nipkow

- Previous by Date: Re: [isabelle] Proof by analogy and proof stability in Isabelle
- Next by Date: Re: [isabelle] Proof by analogy and proof stability in Isabelle
- Previous by Thread: Re: [isabelle] Proof by analogy and proof stability in Isabelle
- Next by Thread: Re: [isabelle] Proof by analogy and proof stability in Isabelle
- Cl-isabelle-users April 2010 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list