From owner-qed Fri Aug 12 12:38:49 1994 Received: from localhost (listserv@localhost) by antares.mcs.anl.gov (8.6.4/8.6.4) id MAA09499 for qed-out; Fri, 12 Aug 1994 12:37:34 -0500 Received: from swan.cl.cam.ac.uk (pp@swan.cl.cam.ac.uk [128.232.0.56]) by antares.mcs.anl.gov (8.6.4/8.6.4) with ESMTP id MAA09491 for ; Fri, 12 Aug 1994 12:37:24 -0500 Received: from merganser.cl.cam.ac.uk (user rjb (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Fri, 12 Aug 1994 18:37:12 +0100 To: dam@ai.mit.edu (David McAllester) cc: qed@mcs.anl.gov Subject: Re: Accept Anarchy In-reply-to: Your message of "Fri, 12 Aug 94 09:52:23 EDT." <9408121352.AA12890@spock> Date: Fri, 12 Aug 94 18:37:06 +0100 From: Richard Boulton Message-ID: <"swan.cl.cam.:229170:940812173715"@cl.cam.ac.uk> Sender: owner-qed@mcs.anl.gov Precedence: bulk David McAllester writes: > 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.