[SystemSafety] Bursting the formal methods bubble

[Peter Bernard Ladkin]

On 2017-10-25 18:08 , Derek M Jones wrote:
>> 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.
> 
> That is not how I interpret what Lamport said:

Better said, that is not how you interpret what he *wrote*. That may well be. I was reporting what
he said in his talk.

> Now we agree that new mathematical 'proofs' often contain bugs,

The proofs produced by formal methods in (real) software development do not in my experience contain
bugs.

One of mine did. I took months to generate a formally rigorous hand proof in TLA of the safety
properties of the Afek-Brown-Merritt lazy caching algorithm. The "action reasoning" had fourteen
clauses. When I was in Montreal in 1995, I went over to Ottowa one day to have Mark Saaltink go over
it with the Eves prover (which is based on first-order set theory, like TLA, so compatible without
translation). Mark blasted thirteen of the fourteen in a couple of hours, allowing me to feel quite
sheepish and close to useless. The fourteenth presented a problem. I went back to Montreal. Then I
realised what the issue was ...... fixed the clause, went back the next day and Mark plasted the
corrected clause in a few minutes. Allowing me to feel no longer close to useless, but indeed
utterly useless.

> can you tell me what the claims about formal methods proving
> correctness actually mean.
Sure I *could*, but I think I'd be wasting my time.

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/292df75f/attachment.sig>