[SystemSafety] Logical difficulties in mathematics

[Peter Bernard Ladkin]

On 2019-02-15 15:07 , Derek M Jones wrote:
> 
> Perhaps somebody ought to tell mathematicians about formal methods.
> 

Leslie Lamport has been on this thirty years ago. I was at a talk he gave in Berkeley in which he
pointed out a mistake in the intro to John Kelley's book Topology, then a pervasive graduate
textbook, which he claimed showed that mathematicians were a lot less careful about proofs than (he
suggested) they ought to be. There ensued a riveting open discussion with VelVel Kahan.

Those were the days! Dick Karp was the only Turing Laureate at the talk, but there were three more
to come - Kahan, Manuel Blum and Leslie.

The debate had the usual content. Let's see if I remember:

LL: Here's the mistake
WK: But it's not important. People who learn topology know how to fix it.
LL: Kelley apparently didn't even know it was wrong; his book has been through a number of editions.
What are we supposed to make of that in terms of rigor in math?
WK: He didn't pay attention to it because his (correct) mathematical intuition told him the general
theme he was addressing was being handled in the right way.
LL: How are students, who don't necessarily have that intuition and are trying to find out if they
do, supposed to handle it? Apparently they all suck it up/have all sucked it up for decades. Glossed
over a mistake because "it's in Kelley". Is this how "rigor" is supposedly taught in mathematics?
Something is missing. Computer scientists now know what rigor is, and much of mathematics does not
have it.
WK: There is nothing really wrong. The people who know the subject gloss over it because it is
generally right and the individual details are a homework exercise, even if they are not correctly
portrayed in the text.

And so on. It is eerily parallel to discussions I have had more recently with engineers in standards
committees: "it might be wrong, but the general idea is *practical*". "If you agree it is wrong,
then why don't you fix it?"

PBL

Prof. Peter Bernard Ladkin, Bielefeld, Germany
MoreInCommon
Je suis Charlie
Tel+msg +49 (0)521 880 7319  www.rvs-bi.de





-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 833 bytes
Desc: OpenPGP digital signature
URL: <https://lists.techfak.uni-bielefeld.de/mailman/private/systemsafety/attachments/20190215/160c849e/attachment.sig>