Return-Path: <John.Harrison-request@cl.cam.ac.uk>
Delivery-Date: 
Received: from antares.mcs.anl.gov (no rfc931) by swan.cl.cam.ac.uk 
          with SMTP (PP-6.5) outside ac.uk; Thu, 29 Apr 1993 14:35:51 +0100
Received: by antares.mcs.anl.gov id AA12134 (5.65c/IDA-1.4.4 for qed-outgoing);
          Thu, 29 Apr 1993 08:22:50 -0500
Received: from linus.mitre.org by antares.mcs.anl.gov with SMTP 
          id AA12127 (5.65c/IDA-1.4.4 for <qed@mcs.anl.gov>);
          Thu, 29 Apr 1993 08:22:48 -0500
Received: from circe.mitre.org by linus.mitre.org (5.61/RCF-4S) id AA05828;
          Thu, 29 Apr 93 09:22:40 -0400
Posted-Date: Thu, 29 Apr 93 09:22:38 -0400
Received: by circe.mitre.org (5.61/RCF-4C) id AA12381;
          Thu, 29 Apr 93 09:22:39 -0400
Message-Id: <9304291322.AA12381@circe.mitre.org>
To: qed@mcs.anl.gov
Subject: Re: Cold water
In-Reply-To: dts@dcs.ed.ac.uk's message of "Thu, 29 Apr 93 12:29:37 BST." <8849.9304291129@harris.dcs.ed.ac.uk>
X-Postal-Address: MITRE, Mail Stop A156 \\ 202 Burlington Rd. \\ Bedford, MA 
                  01730
X-Telephone-Number: 617 271 2654; Fax 617 271 3816
Date: Thu, 29 Apr 93 09:22:38 -0400
From: guttman@linus.mitre.org
Sender: qed-owner@mcs.anl.gov
Precedence: bulk

I think we should look for the first major benefits of
machine-supported rigorous mathematics will be in mathematics
education.

And that means that systems should be very serious about issues such
the ability to take large ("human-sized") proof steps and having a
style of formalization and proof that is very close to the ethos of
traditional rigorous mathematics.

Just as the big pay-off of formal methods for software (and/or
hardware) depend on the normal, well-educated developer being able to
understand how to use them, the impact of formal methods for
mathematics depends on being understandable to a broad range of people
with the normal kind of mathematical culture. 

	Josh