[SystemSafety] Bursting the formal methods bubble

Peter Bernard Ladkin ladkin at causalis.com
Wed Oct 25 17:24:49 CEST 2017


On 2017-10-25 15:15 , Derek M Jones wrote:> Formal methods is founded on the idea that mathematical
> work is always, magically, correct.

Nowhere near the case, neither the idea nor the attribution. For example:-

Leslie Lamport has a talk he gave widely some almost thirty years ago in which he pointed out that
mathematicians are mostly not very good at writing proofs, and that there are lots of mistakes in
published mathematics. He said that anecdotal evidence suggests about a third of all published math
contains mistakes (repeated in the paper below). He quoted a mistake in the intro to John Kelley's
book General Topology, then one of the most widely-used texts for over three decades, to illustrate.

He said that computer scientists had developed much better methods for writing rigorous proofs,
namely formal methods, and recommended their use also in mathematics to avoid mistakes.

Some of this made it into http://lamport.azurewebsites.net/pubs/pubs.html#lamport-how-to-write which
is well worth reading, also just for fun.

(He says in the article he uses "natural deduction". The style of TLA proof he advocated then, and I
used, with the LaTeX proof style package, is the inverse of the Gentzen/Prawitz natural deduction
style.)

> The mathematics we all learn in school/university has been around
> long enough to be throughly checked, which gives people a skewed
> view of mathematics.

Like John Kelley's (then) 30-year-old mistake, I suppose.

Or are we supposed to note a difference in meaning between "around long enough to be thoroughly
checked" and "around long enough to have been thoroughly checked"?

One of the most fun talks I have ever been to was when Leslie gave this one at UC Berkeley. Four
present or future Turing Award winners in the room, three of them primarily mathematicians, all with
somewhat different and well-articulated views on the matter. Followed by entertaining, gossipy dinner.

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/20171025/e7664401/attachment-0001.sig>


More information about the systemsafety mailing list