From owner-qed Thu Oct 27 09:25:06 1994
Received: from localhost (listserv@localhost) by antares.mcs.anl.gov (8.6.4/8.6.4) id JAA23788 for qed-out; Thu, 27 Oct 1994 09:24:05 -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 JAA23780 for <qed@mcs.anl.gov>; Thu, 27 Oct 1994 09:23:56 -0500
Received: (from yodaiken@localhost) by chelm.nmt.edu (8.6.8.1/8.6.6) id IAA12113; Thu, 27 Oct 1994 08:27:21 -0600
Message-Id: <199410271427.IAA12113@chelm.nmt.edu>
From: yodaiken@sphinx.nmt.edu (Victor Yodaiken)
Date: Thu, 27 Oct 1994 08:27:21 -0600
In-Reply-To: Randall Holmes <holmes@catseye.idbsu.edu>
       "Bit strings and semantics" (Oct 26,  4:52pm)
reply_to: yodaiken@chelm.nmt.edu
X-Mailer: Mail User's Shell (7.2.5 10/14/92)
To: Randall Holmes <holmes@catseye.idbsu.edu>, qed@mcs.anl.gov
Subject: Re: Bit strings and semantics
Sender: owner-qed@mcs.anl.gov
Precedence: bulk

On Oct 26,  4:52pm, Randall Holmes wrote:
 Subject: Bit strings and semantics
>
>With a suitable ADT interface, bit strings can be made to look
>like objects of the most amazing and diverse sorts!!!  (lists
>(even infinite ones!), trees, formulas of your favorite language,
>arbitrary-precision integers, maybe even ZFC sets :-)
>
>So the argument against the semantic, non-formalist attitude is
>belied by C. S. practice.  We are not exhorted to remember that objects
>of the usual CS types are implemented as bit strings in various odd
>ways -- in fact, we are usually supposed to forget this!!!

With dismal consequences for those who mistake floats for real
numbers, for example. In any case, I don't want to make an argument
for "formalism", I just want to recall that any theorem proving
program will, ultimately, just be shuffling syntax.