From owner-qed Fri Aug 12 11:27:32 1994
Received: from localhost (listserv@localhost) by antares.mcs.anl.gov (8.6.4/8.6.4) id LAA07360 for qed-out; Fri, 12 Aug 1994 11:25:58 -0500
Received: from chelm.nmt.edu (chelm.nmt.edu [129.138.6.50]) by antares.mcs.anl.gov (8.6.4/8.6.4) with ESMTP id LAA07353 for <qed@mcs.anl.gov>; Fri, 12 Aug 1994 11:25:50 -0500
Received: (from yodaiken@localhost) by chelm.nmt.edu (8.6.8.1/8.6.6) id KAA09151; Fri, 12 Aug 1994 10:28:53 -0600
Message-Id: <199408121628.KAA09151@chelm.nmt.edu>
From: yodaiken@sphinx.nmt.edu (Victor Yodaiken)
Date: Fri, 12 Aug 1994 10:28:53 -0600
In-Reply-To: dam@ai.mit.edu (David McAllester)
       "Accept Anarchy" (Aug 12,  9:52am)
reply_to: yodaiken@chelm.nmt.edu
X-Mailer: Mail User's Shell (7.2.5 10/14/92)
To: dam@ai.mit.edu (David McAllester), qed@mcs.anl.gov
Subject: Re: Accept Anarchy
Sender: owner-qed@mcs.anl.gov
Precedence: bulk

On Aug 12,  9:52am, David McAllester wrote:
 Subject: Accept Anarchy
>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.

Bravo.  I'm no fan of complex type theories, but it is important to
realize that just because one _can_ encode a part of mathematics inside
another, it does not mean that one should.