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




"Transferring content" is exactly what an external representation of
proof objects would allow you to do. A format like Joe Hurd's
OpenTheory is designed primarily for transferring theorems between
completely different theorem provers, but the same idea could also be
useful for transferring theorems between different versions of the
*same* theorem prover.

And yes, this means
that at least a part of the versioning system becomes part of the trusted kernel
of the proof assistant.

The great thing about using proof objects is that you don't need to
trust any new code.


I think these issues should be transparent for the end user of the proof assistant. It is maybe a good idea to use proof objects for implementing the versioning system, but special cases like a change in the proof object format (and there will be changes, trust me) and so on must then be handled transparently by the system, otherwise it becomes a pain for the user. Also proof objects are big and slow; most users are willing to trade a vastly improved user experience for a little bit of trust ...

My point is just that earlier snapshots of the theory development of a theorem prover should be accessible from the current theory development, no matter how that is implemented exactly. As an example, take the theory of the real numbers.

A simple way of approaching this is to first introduce the natural numbers, then rational numbers, then the real numbers. Later on we introduce new natural numbers, new rational numbers and so on, so that they are now subsets of each other. Actually, there is no need now any more for the original natural numbers and so on. With a versioning system we can throw them out of our newest version. In our newest version, we can axiomatically introduce the real numbers (and justifying this by pointing to the definition in an earlier version). Also, there are several ways of introducing the real numbers. This is no problem in our system, each way could belong to a different version.

So for the user, stuff that has been done 10 years ago, is still there, unchanged, and it is accessible from the newest version of the system. It is important that the versioning system is elegant and easy to understand. It provides the high-level view of how the user thinks about the system.

- Steven




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