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 <qed@mcs.anl.gov>; 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