Re: Cold water
guttman@linus.mitre.org
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
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