> I do not support any standard language for describing systems.
> Such a language seems just as difficult and controversial as a
> standard verification language. It seems to me that, ideally, each system
> developer should make some attempt to provide translators into and
> out of other languages. In this way we can develop a distributed
> "translation web". I think that over time a small set of standard
> languages will become widely used as "interlingua".
I'm not sure what you are opposing here, but if I'm reading it correctly you
don't think the QED system should have a standard format for its data.
It would not be impossible to implement this way but it would mean that any
"browser" would have to take a very hands-off approach, doing little more
than traversing the network and executing other programs. The bulk of the
operations would have to be implemented separately for each formal system.
Introducing a new formal system would then require a lot more effort, but
perhaps this is not a bad thing as it might discourage too much diversity.
To be a little more concrete I am envisaging something like this:
Somehow the browser is guided to a proof somewhere on the network.
The proof is labelled as being in John-Doe's-proof-system (call it JD).
The browser then looks up JD in an index of proof systems, finds where
it is defined on the network, and downloads the programs that support
the JD proof system. (Note: it downloads *programs* not data since as
there is no common format data would be meaningless to it.)
The programs allow the user to display, store, proof-check, etc., the
proof. If the user wants the theorem in another proof system then
a translator between the two systems (if there is one) must be found
and loaded, as well as the support functions for the second system
so that the translated theorem can be operated on.
The only standard possibly required for this is what abstract operations
(display, store, proof-check, translate) QED should support.
Is this anything like what you had in mind?
> I would also like to avoid centralized "certification" of the
> soundness of systems. Unsound systems will get bad reputations.
If nothing is done to protect less well-informed users it may be the entire
QED venture that gets a bad reputation not just unsound systems. However,
there are lots of ways to deal with this without using centralized
certification, and I can see that there would be problems with such
certification.
Richard.