-
Notifications
You must be signed in to change notification settings - Fork 0
Chapter 10 Proof Track
When writing proofs of properties of systems or algorithms, we should not look at mathematicians’ proofs for models. There are three reasons why the way (almost all) mathematicians write proofs do not work for our proofs:
- The theorems mathematicians prove are very different from what we are proving. Mathematical theorems are usually deep, being based on knowledge that has been developed over centuries. Our theorems are shallow but wide.
What does this mean? Shallow but wide?
They generally use only simple mathematics, but require checking many details.
- Mathematicians don’t care if their theorems are not quite correct. Omitting a simple hypothesis such as that a certain set is nonempty would not even be considered an error. For the proof of an algorithm, such an omission means a bug in a "corner case".
- The proofs mathematicians write are unreliable. Anecdotal evidence suggests that a significant fraction of published, refereed mathematical papers contain incorrect theorems|not ones ignoring corner cases, but results that mathematicians would consider wrong. Based on a tiny amount of data, I would guess that fraction to be more than a tenth. (This includes results that have a correct proof but are wrong because the proof relies on theorems that are wrong.)
Mathematicians depend on the social process to weed out incorrect results. Most theorems are ignored and soon forgotten. The few important results are scrutinized by many mathematicians, and errors in them are eventually discovered. Two false 19th century proofs of the four-color theorem were believed for 11 years. However, the greater number of mathematicians and improved communications make it very likely that an incorrect proof of such a major result would today be quickly discovered.
When a mathematician’s style of proof is used to prove properties of systems, the result is often disastrous. There is no social process to find errors an engineer makes in a proof of a system she is designing. Even for published algorithms, the social process doesn’t work very well. One dramatic example is provided by: Pamela Zave. Lightweight verification of network protocols: The case of Chord. AT&T Technical Report, January 2010. The Chord algorithm was first published in:
?✛ - C I SI. Stoica, R. Morris, D. Karger, M. F. Kaashoek, and H. Balakrishnan. Chord: A scalable peer-to-peer lookup service for Internet applications. Proceedings of SIGCOMM. ACM, August 2001.
This paper states: Three features that distinguish Chord from many other peer-to-peer lookup protocols are its simplicity, provable correctness, and provable performance.
However, Zave reports: [T]he Chord routing protocol is neither proven nor correct. The only published proof of correctness excludes failures from consideration. Even within its scope the proof does not compel belief, due to ill-defined terms and missing or unjustified steps. The full protocol is clearly incorrect, even after bugs with straightforward fixes have been eliminated. Not one of the six properties claimed invariant for the full protocol . . . is invariantly true.
What would the TLAPS vs the LEAN specification of this protocol be?
Chord is quite well known. A web search on its title yields many thousands of references. The paper won a SIGCOMM Test of Time Award in 2011. Yet, the errors in the algorithm went unnoticed for almost 10 years. Zave found them by writing a formal specification of the algorithm (in the Alloy language) and applying a form of model checking. What distinguishes Chord from most published algorithms is that someone applied formal methods to check if it really was correct.
When would I use LEAN vs a system like TLAPS?
One way to make hand proofs more reliable is to structure them hierarchically. The Principles track of this hyperbook uses such structured proofs.
Structuring is equally important in handling the complexity of a formal proof, and formal proofs written in TLA+ are hierarchically structured.