Pink Iguana

Home » References » Proofs and Verifications

Proofs and Verifications


DeMillo, Lipton, and Perlis, Social Processes and Proofs of Theorems and Programs, 1979, here.

It is argued that formal verifications of programs, no matter how obtained, will not play the same key role in the development of computer science and software engineering as proofs do in mathematics. Furthermore the absence of continuity, the inevitability of change, and the complexity of specification of significantly many real programs make the formal verification process difficult to justify and manage. It is felt that ease of formal verification should not dominate program language design.

forgot about this, I don’t know who wrote this line:

To put it another way, the severity with which a system fails is directly proportional to the intensity of the designer’s belief that it cannot fail.

William P. Thurston, On Proof and Progress in Mathematics, 1994, here.

Peter Woit, Not Even Wrong, Latest on abc, here. Woit’s on fire.

In case you haven’t been following this story, “abc” refers to a famous conjecture in number theory, for which Shin Mochizuki claimed last year (see here) to have found a proof. His argument for abc involves a new set of ideas he has developed that he calls “Inter-Universal Teichmuller Theory” (IUTeich). These are explained in a set of four papers with a total length over 500 pages. The papers are available here, and he has written a 45 page overview here. One can characterize the reaction to date of most experts to these papers as bafflement: what Mochizuki is doing is just so far removed from what is known and understood by the experts that they have no way of evaluating whether or not he has a new idea that solves the abc problem.

Trust the math? An Update, here.

Update: There’s a response to the Reuters story from RSA here. As I read it, it says

  • They do have a secret contract with the NSA that they cannot discuss
  • They used the NSA back-doored algorithm in their product because they trust the NSA
  • They didn’t remove it when it became known because they really are incompetent, not because the NSA was paying them to act incompetent

Andrew W. Appel, Verifiable C, 2013, here. Wow with the Crypto Theorem Shaving allegations it looks like Verification scores on a Hail Mary pass.

This summary reference manual is a brief guide to the VST Separation Logic for the C language. The Verified Software Toolchain and the principles of its program logics are described in the book:

Program Logics for Certified Compilers, by Andrew W. Appel et al., Cambridge University Press, 2014.


Leave a Reply

Fill in your details below or click an icon to log in: Logo

You are commenting using your account. Log Out /  Change )

Google+ photo

You are commenting using your Google+ account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )


Connecting to %s

%d bloggers like this: