Return-Path: Delivery-Date: Received: from antares.mcs.anl.gov (no rfc931) by swan.cl.cam.ac.uk with SMTP (PP-6.5) outside ac.uk; Tue, 20 Apr 1993 16:48:48 +0100 Received: by antares.mcs.anl.gov id AA16693 (5.65c/IDA-1.4.4 for qed-outgoing); Tue, 20 Apr 1993 10:30:00 -0500 Received: from swan.cl.cam.ac.uk by antares.mcs.anl.gov with SMTP id AA16681 (5.65c/IDA-1.4.4 for ); Tue, 20 Apr 1993 10:29:50 -0500 Received: from dunlin.cl.cam.ac.uk (user lcp (rfc931)) by swan.cl.cam.ac.uk with SMTP (PP-6.5) to cl; Tue, 20 Apr 1993 16:29:23 +0100 To: qed@mcs.anl.gov Subject: Different Schools Date: Tue, 20 Apr 93 16:29:09 +0100 From: Lawrence C Paulson Message-Id: <"swan.cl.cam.:080740:930420152927"@cl.cam.ac.uk> Sender: qed-owner@mcs.anl.gov Precedence: bulk Translation (or interpretation) between different schools is one of the key issues. We also need translation to import theories from other systems. A common "lingua franca" could be valuable; it is another of the key issues. Should this merely formalize assertions, or should it also capture aspects of their proofs, like the "mathematical vernacular" (de Bruijn's concept)? Making the "lingua franca" neutral will not be easy. The if-then-else construct, descriptions and powersets are unacceptable in certain schools. I also fear disagreement on whether the "lingua franca" should be typed or untyped (I prefer the latter). Larry Paulson