Re: Cold water
Message-id: <>
Subject: Re: Cold water 
In-reply-to:'s message of "Thu, 29 Apr 93 12:29:37 BST."
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
Sender: qed-owner
Precedence: bulk
I think we should look for the first major benefits of
machine-supported rigorous mathematics will be in mathematics

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.