[SystemSafety] Practical problems using coq for formal verification

[Peter Bernard Ladkin]

On 2017-12-27 14:56 , Derek M Jones wrote:
> A insightful take on the problems of using Coq for formal verification:
> https://raywang.tech/2017/12/20/Formal-Verification:-The-Gap-between-Perfect-Code-and-Reality/
It's cute to see an MITer complaining when 2,000 LOC becomes 20,000. I thought it was a rule there
that, if you couldn't do that, you failed the course. (Key exhibit: Lisp to Lisp machines.)

And describing four-figure CoQ-LOC sums as "overhead". How very quaint. Nowadays we'd call that
"underflow".

The writer notes that some partially-verified systems can still have bugs. Surely pretty obvious,
once you think about it? Like the clerk pointing out that your day-return ticket won't be valid for
the 07:30 train you might want to catch? In any case, I would agree it seems a good idea to point
this out to people with limited experience.

He points out that no errors were found in implementations of the Paxos collection of algorithms in
an "empirical study" and says this shows that "verification <i>can</i> be applied to increase
reliability". You betcha. Back in the day (80's once again) people used three-phase commit, and
Skeen showed it didn't work. People carried on using it because they didn't have anything better and
Skeen's observation was rationalised as "theory". Then Lamport derived the first Paxos algorithm.
You will find no stronger proponent of formally proving that your algorithms are correct than
Leslie. Nowadays, Paxos algorithms are ubiquitous and form much of what keeps Google, Facebook and
Amazon running around the world. And that is supposed to be a sidebar to an argument that formal
verification doesn't do what you want? Surely it is a good example of exactly the contrary.

I wonder if it's actually someone older trying to fake being a disgruntled student? :-)
Maybe you, Derek? :-)

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/20171227/1217b464/attachment.sig>