From owner-qed Fri Aug 12 08:53:36 1994 Received: from localhost (listserv@localhost) by antares.mcs.anl.gov (8.6.4/8.6.4) id IAA02690 for qed-out; Fri, 12 Aug 1994 08:52:32 -0500 Received: from life.ai.mit.edu (life.ai.mit.edu [128.52.32.80]) by antares.mcs.anl.gov (8.6.4/8.6.4) with SMTP id IAA02685 for ; Fri, 12 Aug 1994 08:52:27 -0500 Received: from spock (spock.ai.mit.edu) by life.ai.mit.edu (4.1/AI-4.10) for qed@mcs.anl.gov id AA24802; Fri, 12 Aug 94 09:52:24 EDT From: dam@ai.mit.edu (David McAllester) Received: by spock (4.1/AI-4.10) id AA12890; Fri, 12 Aug 94 09:52:23 EDT Date: Fri, 12 Aug 94 09:52:23 EDT Message-Id: <9408121352.AA12890@spock> To: qed@mcs.anl.gov In-Reply-To: Richard Boulton's message of Fri, 12 Aug 94 12:52:31 +0100 <"swan.cl.cam.:085270:940812115246"@cl.cam.ac.uk> Subject: Accept Anarchy Sender: owner-qed@mcs.anl.gov Precedence: bulk I will add my vote for diversity. When this list started I sent a variety of messages supporting a "multilingual" approach. I also agree that "the library" should be distributed across the net and accessible through mosaic and WWW. 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 do not think that developers will choose to build translators to and from raw set theory. Raw set theory does not maintain the "structure" of theorems. Structure is essential in heuristically guiding verification. For example, many verifications rely on type checking algorithms. Raw set theory does not distinguish types from other formulas. I would also like to avoid centralized "certification" of the soundness of systems. Unsound systems will get bad reputations. Confidence in a theorem should be established by verifying it with systems that have good reputations or by verifying it in several different systems. David