An Unverifiable World1. The Luxury of VerificationContents中文

Chapter 1: The Luxury of Verification

Thesis: Complete verification, the kind that confirms in advance that something is true, correct, or safe, is the exception in the lives of people and machines, not the rule.

Seven Times Eight, and Everything Else

You can verify that seven times eight is fifty-six. You can count it again, work it out another way, or just recite the times table. Within seconds, the answer is settled.

Now try a few other things. Before you say "I do," verify that the marriage will last. Before you hit deploy, verify that the code has not a single bug. Before you give half your life to a theory, verify that it is true. Before you take the job, verify that the company is healthy. You cannot do any of these. That is not because you have not tried hard enough. It is because things like these simply do not offer the option of checking in advance.

That contrast is the first cornerstone of this book: complete verification, the kind that confirms in advance that something is true, right, or safe, is the exception in the lives of people and machines, not the rule. It only feels like the rule because our intuitions were formed inside a very narrow door.

The Narrow Door Where Checking Is Cheap

What can we actually verify? Working an arithmetic problem, sorting a list of numbers, checking the total on a receipt, deciding whether a move on the board is legal. Put these side by side and they share a few hidden features. The object is closed: everything relevant is in front of you. It is finite: you can count the cases. The answer is local and immediate: it does not depend on anything far away or in the future. And there is a mechanical procedure that gives you a yes or a no if you follow it.

This narrow door is what feeds our intuition that "everything can be checked." School rewards exactly this kind of problem, over and over: one with a standard answer that can be marked on the spot. So we quietly stretch a piece of experience ("in the things I have practiced, right and wrong can always be sorted out") into a worldview ("right and wrong can always be sorted out"). That stretch is wrong, and wrong in a systematic way. Outside the narrow door, nearly every one of those four features fails.

Four Places the Illusion Breaks

Verification: the cheap narrow door, and the four breaches outside it

Scale. Inside the door you can count the cases; outside, you cannot. A program with $n$ branches can have as many as $2^n$ execution paths, and a few dozen branches are enough to make exhaustive testing impossible to finish within the lifetime of the universe. This path explosion rules out "test everything" from the start. You can verify that a program is correct on the handful of inputs you thought of. You cannot verify that it is correct on all of them. On August 1, 2012, Knight Capital deployed new trading software, but one of its eight servers was never updated. A reused flag accidentally woke a stretch of old code that had sat dormant, long deprecated, for years. In roughly forty-five minutes after the opening bell it fired off millions of orders, cost the firm about 440 million dollars, and nearly bankrupted it overnight. No one had verified that dead code path, because no one imagined it would ever run again. Checking one case is easy. The moment the word "all" appears, you are in a different world.

Open world. Inside the door the object is closed; outside, the world keeps sending new things. What you tested was a small set of scenarios. What the system actually meets is an open environment that keeps unfolding. On June 4, 1996, the Ariane 5 rocket made its first flight and destroyed itself about thirty-seven seconds after launch. The cause was inertial navigation code carried over unchanged from the Ariane 4 and never re-verified for the new trajectory. It forced a 64-bit floating-point number into a 16-bit integer, and the new rocket's higher horizontal velocity made that number overflow. Counting the four scientific satellites on board, the loss exceeded 370 million dollars. The code had run correctly for years in the old world; in the new one it was lethal. The MCAS system on the Boeing 737 MAX is a more harrowing case of the same break. It behaved normally in test flight after test flight, yet on real routes it acted on a single faulty angle-of-attack sensor and pushed the nose down again and again. Two crashes (Lion Air 610 in 2018 and Ethiopian 302 in 2019) killed 346 people. What you verify is always a slice of what you have already seen. What you have to bet on is a future you have not.

Other minds. Inside the door you can observe the state; outside, the goal you have to satisfy is often locked inside someone else's head. The familiar complaint "you built it right, but it isn't what I wanted" starts here. What the user really wants, whether your boss is satisfied, whether the other person loves you: these are latent variables. You can only infer them indirectly, from behavior. You cannot read them off directly, so you cannot directly verify whether you have satisfied them. Even life's most solemn commitments are not exempt. By demographic estimates, roughly forty to fifty percent of first marriages in the United States end in divorce, and no one saying "I do" can verify that theirs will last.

The future. This is the deepest break, and Hume laid it out as early as 174817: induction has no logical guarantee. The sun has risen every day so far, but that does not logically prove it will rise tomorrow. No finite amount of past experience can verify in advance a universal claim about the future. What we rely on is habit, not proof. Every action whose outcome lies in the future (a marriage, an investment, a crop in the ground, trust placed in someone) sits on the far side of this break.

Not Even Math and Software Are Exempt

You might accept all this for messy things like scale, other people, and the future, and still expect mathematics and software to be different. Surely those, at least, can be checked completely? In fact, these two fields have been the most clear-eyed about where checking runs out.

On the software side, Dijkstra left a line that has been quoted endlessly and is still true: testing can show the presence of bugs, but never their absence14. He argued that a program should be built correct, not debugged into correctness13. Yet even formal proof, the strictest route, has limits. In a famous and contested 1979 paper9, DeMillo, Lipton, and Perlis argued that program verification cannot play the role that proof plays in mathematics, because its credibility ultimately comes from a social process, not from mechanical deduction. Fetzer went further in 198810. A program, he argued, is a causal model, separated by a gulf from the algorithm as a logical structure, so "completely reliable program verification" is impossible even in theory. Brooks's "No Silver Bullet"11 holds that no single breakthrough can remove the essential complexity of software. Parnas resigned as an adviser to the Star Wars program and argued publicly that the software for such systems could never be verified well enough to deserve trust12. And the Therac-25 radiotherapy machine is the footnote to all of these warnings, paid for in lives. Between 1985 and 1987 a concurrency bug (a race condition) made it malfunction six times, delivering roughly a hundred times the normal dose of radiation to patients and killing at least three of them15. A 1968 NATO conference coined a name for all this: the software crisis16.

Mathematics cuts deeper still. In 1931 Gödel proved3 that any consistent formal system rich enough to express basic arithmetic contains true statements it cannot decide from within. In 1936 Church and Turing each proved21 that no algorithm can decide whether an arbitrary statement is provable (the Entscheidungsproblem has no solution). Rice's theorem4 took this to its limit: every nontrivial semantic property of programs is undecidable. And even where a problem can be decided in principle, the NP-completeness that Cook established in 19715 shows that the cost of checking can blow up until it is useless in practice. These are not temporary engineering shortcomings. They are hard boundaries that logic draws around verification. The next chapter takes this layer apart on its own.

Not a Counsel of Despair

Put it all together: most actions that matter are taken on unverified ground.

That conclusion should not paralyze you. It is a starting point. Admitting that verification is a luxury is the first step toward taking action seriously. As early as 1921, Knight separated measurable "risk" from unmeasurable "uncertainty"22 and argued that profit comes from the second. Keynes, writing about genuine uncertainty, could only say "we simply do not know"26. Simon, seeing that a bounded actor cannot check every option exhaustively, proposed "satisficing"23. Von Neumann and Morgenstern, and Savage, each built a formal framework for betting rationally when outcomes cannot be verified in advance2425. A whole discipline of decision-making rests on the premise that verification is unavailable. The question was never how to abolish uncertainty. It was how to act well inside it.

What Comes Next

If verification is usually out of reach, the first question is why.

There is more than one answer, and that is the point. Treating "I cannot check it" as one situation is the most common and most misleading mistake in this field. It is really five structurally different situations hiding behind one sentence. The next chapter breaks that sentence into five.

Next chapter: 2. The Five Faces of Unverifiability →← Preface: A World Without Oracles

References

Waypoints: 1. historical scientific judgment; 2. theoretically studied material; 3. how science progresses; 4. how to live in an unverifiable world. This section was checked source by source.

  1. A. M. Turing (1936). "On Computable Numbers, with an Application to the Entscheidungsproblem." Proceedings of the London Mathematical Society, s2-42, 230-265. doi:10.1112/plms/s2-42.1.230 [2] Turing, modeling computation with an abstract machine, proved that no algorithm can decide whether an arbitrary proposition is provable, and from this derived the undecidability of the halting problem. This is the founding work that raised the limit of verification from engineering experience to a mathematical theorem; the section "Not Even Math and Software Are Exempt" uses it precisely to show that the Entscheidungsproblem has no solution. The series 2, volume 42 in which it appears spans 1936 to 1937, and some bibliographies date it to 1937; the text uses the conventional 1936.

  2. A. Church (1936). "An Unsolvable Problem of Elementary Number Theory." American Journal of Mathematics, 58(2), 345-363. doi:10.2307/2371045 [2] Church, using the lambda calculus he founded, independently proved that elementary number theory contains an unsolvable decision problem, publishing several months before Turing. His work converges with Turing's by a different route, jointly framing the theoretical boundary of "what is computable," and reminds the reader that the unavailability of verification was established along two independent paths in 1936.

  3. K. Gödel (1931). "Über formal unentscheidbare Sätze der Principia Mathematica und verwandter Systeme I." Monatshefte für Mathematik und Physik, 38, 173-198. doi:10.1007/bf01700692 [2] Gödel proved that any sufficiently rich and consistent formal system contains true propositions it can neither prove nor refute. This means that "verifying every truth one by one inside the system" is impossible in principle, the deepest cornerstone of this chapter's argument that verification has a hard boundary, and one the next chapter takes apart on its own.

  4. H. G. Rice (1953). "Classes of Recursively Enumerable Sets and Their Decision Problems." Transactions of the American Mathematical Society, 74, 358-366. doi:10.1090/s0002-9947-1953-0053041-6 [2] Rice's theorem pushes the undecidability of the halting problem to its limit: no general decision algorithm exists for any nontrivial semantic property of a program. It tells the reader that questions about "what this program will actually do" are almost uniformly not mechanically verifiable, the key support for this chapter's passage on how even the hardest fields bow.

  5. S. A. Cook (1971). "The Complexity of Theorem-Proving Procedures." Proceedings of the 3rd Annual ACM Symposium on Theory of Computing (STOC), 151-158. doi:10.1145/800157.805047 [2] Cook here established the concept of NP-completeness, proving that the satisfiability problem carries a universal computational hardness for a large class of problems. It reveals another limit of verification: even when a problem is decidable in principle, the cost of solving or checking it may explode until it simply cannot run in practice, matching this chapter's account of how "scale" fails.

  6. C. A. R. Hoare (1969). "An Axiomatic Basis for Computer Programming." Communications of the ACM, 12(10), 576-580. doi:10.1145/363235.363259 [2][1] Hoare proposed an axiomatic system, later called Hoare logic, for rigorously proving program correctness with preconditions, postconditions, and inference rules. It represents the ambition of the strictest line, to carry verification all the way through, and lets the reader see both how far formal verification can go and why, in engineering reality, it has always struggled to cover everything.

  7. J. C. King (1976). "Symbolic Execution and Program Testing." Communications of the ACM, 19(7), 385-394. doi:10.1145/360248.360252 [2] King proposed symbolic execution: replacing concrete inputs with symbolic variables and systematically deriving, along a program's branches, the conditions each path must satisfy. The technique both widened the coverage of automated testing and laid bare the "path explosion" in which the number of paths grows exponentially with branches, the very difficulty this chapter uses to explain why exhaustive verification is limited.

  8. E. M. Clarke and E. A. Emerson (1981). "Design and Synthesis of Synchronization Skeletons Using Branching Time Temporal Logic." Logics of Programs (Lecture Notes in Computer Science 131), Springer, 52-71. doi:10.1007/BFb0025774 [2] This workshop paper proposed using branching-time temporal logic to check automatically whether a system satisfies a given property, founding model checking. It represents the branch in which machine verification truly landed, but its power presumes a finite system state, and so it draws exactly the boundary between what automated verification can reach and what it cannot. The paper appears in LNCS volume 131, a conference proceedings rather than a journal.

  9. R. A. DeMillo, R. J. Lipton, and A. J. Perlis (1979). "Social Processes and Proofs of Theorems and Programs." Communications of the ACM, 22(5), 271-280. doi:10.1145/359104.359106 [1][2] The three authors argue that mathematical proof is credible because of the social process by which the mathematical community repeatedly reads, reuses, and tests it, whereas the long and mechanical verification of programs lacks such a process and therefore cannot play the role of mathematical proof. This is the famous challenge to the idea that formal verification can give software certainty, cited here to show that the credibility of verification ultimately comes from the social rather than from pure mechanical deduction.

  10. J. H. Fetzer (1988). "Program Verification: The Very Idea." Communications of the ACM, 31(9), 1048-1063. doi:10.1145/48529.48530 [1][2] Fetzer pushed the challenge deeper: an algorithm is a logical structure and can be rigorously proved, whereas a program running on a real machine is a causal model whose behavior is bound by hardware and the world, and between the two lies an unbridgeable gulf. On this basis he argued that "a completely reliable program verification" does not hold even in theory. The paper set off a large-scale debate in the 1989 Technical Correspondence, and is an important part of this chapter's demarcation of the logical boundary of verification.

  11. F. P. Brooks (1987). "No Silver Bullet: Essence and Accidents of Software Engineering." IEEE Computer, 20(4), 10-19. doi:10.1109/mc.1987.1663532 [1] Brooks distinguishes the essential complexity of software from the accidental, asserting that no single technique can yield an order-of-magnitude gain in software productivity within a decade, because essential complexity cannot be eliminated by one stroke. It supports this chapter's judgment that defects cannot be verified away in a single blow by some silver bullet. The piece was originally an invited paper for the 10th IFIP World Computer Congress in 1986, first published in Information Processing 86, 1069-1076.

  12. D. L. Parnas (1985). "Software Aspects of Strategic Defense Systems." Communications of the ACM, 28(12), 1326-1335. doi:10.1145/214956.214961 [1] Parnas, after resigning as an adviser to the Star Wars program, wrote to argue point by point that the software of such systems cannot be verified, by testing or by proof, to a degree worthy of trust. This is a top engineer's public judgment on the limits of verification, made at the cost of his resignation, cited in this chapter as a real-world footnote to how even the hardest fields bow. That same year he also published a series of short essays in American Scientist.

  13. E. W. Dijkstra (1972). "The Humble Programmer" (1972 ACM Turing Award Lecture). Communications of the ACM, 15(10), 859-866. doi:10.1145/355604.361591 [1] This is Dijkstra's Turing Award lecture, arguing that the programmer should stay humble, face the limited capacity of the human mind, and treat a program as something that ought to be correctly constructed rather than patched into correctness after the fact. It reflects a founder's sober judgment on the limits of after-the-fact verification, in resonance with this chapter's claim.

  14. E. W. Dijkstra (1972). Notes on Structured Programming (in O.-J. Dahl, E. W. Dijkstra, C. A. R. Hoare, eds., Structured Programming). Academic Press. Google Books [1] This chapter's much-quoted yet still-correct line, "testing can only prove the presence of defects, never their absence," comes from here. Dijkstra sets out structured programming systematically, arguing that correctness is gained through disciplined construction rather than exhaustive testing. The claim first appeared in manuscript EWD249 (1970) and was formally published in Structured Programming in 1972.

  15. N. G. Leveson and C. S. Turner (1993). "An Investigation of the Therac-25 Accidents." IEEE Computer, 26(7), 18-41. doi:10.1109/mc.1993.274940 [1][4] The two authors give an authoritative investigation of the series of accidents in which the Therac-25 radiotherapy machine, through a software defect, overdosed patients with radiation and even killed them, analyzing the chained causes of race conditions, excessive trust in software, and the absence of an independent safety mechanism. At the cost of human lives it shows what follows when a safety-critical system is put into use without adequate verification, a heavy footnote to this chapter on the cost of verification.

  16. P. Naur and B. Randell (eds.) (1969). Software Engineering: Report on a Conference Sponsored by the NATO Science Committee. Scientific Affairs Division, NATO. link [1] This conference report records practitioners' collective anxiety that the software of the time was routinely late, over budget, and hard to deliver reliably; the term "software crisis" and the very idea of "software engineering" as a discipline came from it. It is the source of this chapter's phrase "software crisis," concentrating a generation of engineers' judgment that software could not be reliably verified. The conference was held in Garmisch, Germany, in October 1968, and the report was published in 1969.

  17. D. Hume (1748). An Enquiry Concerning Human Understanding. (London). Google Books [4][3] Hume here laid bare the problem of induction: to infer from "it has repeatedly been so in the past" that "it will still be so in the future" carries no logical guarantee; whether the sun will rise tomorrow cannot be proved in advance, and people act as usual out of habit, not proof. This is the source of the "future" breach in this chapter, and a starting point the whole book returns to. The 1748 first edition was originally titled Philosophical Essays Concerning Human Understanding, changed to the present title in 1758.

  18. K. Popper (1959). The Logic of Scientific Discovery. Hutchinson. Google Books [3] Popper set out falsificationism systematically: a scientific theory cannot be empirically verified, only falsified, so falsifiability becomes the line between science and non-science, and science advances precisely by trying again and again to overturn theories. It bears directly on this chapter's waypoint "how science progresses," revealing that even science does not accumulate by positive verification. The English edition was expanded by the author from the German original Logik der Forschung (printed 1934, copyright page marked 1935).

  19. W. V. O. Quine (1951). "Two Dogmas of Empiricism." The Philosophical Review, 60(1), 20-43. doi:10.2307/2181906 [3] Quine attacks the two dogmas of empiricism, the sharp analytic-synthetic divide and reductionism, and proposes holism: a theory is a web of belief that meets experience as a whole, and no single statement can be verified or refuted in isolation. It shows that evidence underdetermines theory, deepening this chapter's discussion of how science progresses and why verification cannot be done statement by statement.

  20. T. S. Kuhn (1962). The Structure of Scientific Revolutions. University of Chicago Press. Google Books [3] Kuhn introduced the concept of the paradigm, describing how science alternates between the accumulation of normal science and the crisis brought on by accumulated anomalies, finally undergoing revolution through a paradigm shift. His point is that science does not advance by the stepwise verification of truth in linear accumulation, but through incommensurable paradigm leaps. It gives this chapter's "how science progresses" a picture complementary to, and in contrast with, Popper's.

  21. I. Lakatos (1976). Proofs and Refutations: The Logic of Mathematical Discovery (J. Worrall and E. Zahar, eds.). Cambridge University Press. doi:10.1017/cbo9781139171472 [3][2] Lakatos, through a classroom dialogue tracing the evolution of Euler's formula for polyhedra, shows how mathematical concepts and theorems grow in the back-and-forth of counterexample, re-proof, and revised definition. It overturns the impression that a mathematical proof is a once-and-for-all verification, suggesting that even the most certain field advances through criticism, echoing this chapter's general account of the limits of verification.

  22. F. H. Knight (1921). Risk, Uncertainty and Profit. Houghton Mifflin. Google Books [4] Knight separates "risk," measurable by probability, from genuine "uncertainty," which cannot be measured at all, and argues that the entrepreneur's profit comes precisely from bearing the latter. This distinction is the key to this chapter's turn, after admitting that verification is a luxury, toward a theory of action; it explains how decision and reward acquire meaning when outcomes cannot be verified in advance.

  23. H. A. Simon (1955). "A Behavioral Model of Rational Choice." The Quarterly Journal of Economics, 69(1), 99-118. doi:10.2307/1884852 [4] Simon proposed a behavioral model of bounded rationality: an actor limited in both information and computational power cannot exhaustively compare all options, and can only set an adequate level, stopping at the first option that meets it, which is to satisfice. This is one concrete answer to this chapter's question of how to act well within uncertainty, turning the unavailability of verification into an operable decision rule.

  24. J. von Neumann and O. Morgenstern (1944). Theory of Games and Economic Behavior. Princeton University Press. Google Books [4] The two authors founded game theory and derived expected utility from a set of axioms, arguing that a rational actor should choose according to expected utility. It built a formal framework for how to bet rationally when the opponent's intent and the outcome cannot be verified in advance, one of the pillars of the discipline of decision, built on the unavailability of verification, that this chapter describes.

  25. L. J. Savage (1954). The Foundations of Statistics. John Wiley & Sons. Google Books [4] Savage built axiomatic foundations for subjective probability and personalist decision theory, proving that as long as preferences satisfy certain consistency conditions, an actor behaves as if maximizing expected utility under some subjective probability and utility. It gives a standard of rationality for betting consistently in a world where probabilities cannot be objectively verified, and together with von Neumann's framework it supports this chapter's discussion of decision under uncertainty.

  26. J. M. Keynes (1937). "The General Theory of Employment." The Quarterly Journal of Economics, 51(2), 209-223. doi:10.2307/1882087 [4] Keynes, replying to critics of the General Theory, stressed that genuine uncertainty cannot be measured by probability, that of some things "we simply do not know." He pointed out that an investment decision, facing an unverifiable future, can only rely on convention and animal spirits. This chapter's classic statement of genuine uncertainty comes from here, and it corroborates that the discipline of decision takes the unavailability of verification as its premise.

  27. A. Tversky and D. Kahneman (1974). "Judgment under Uncertainty: Heuristics and Biases." Science, 185(4157), 1124-1131. doi:10.1126/science.185.4157.1124 [4] Tversky and Kahneman showed experimentally that in judging probability people often rely on heuristic shortcuts such as representativeness, availability, and anchoring, and so deviate systematically from the norms of probability. It completes this chapter's picture at the descriptive level: in a world where probability cannot be fully verified, how people actually judge, and where they consistently go wrong.

  28. N. N. Taleb (2007). The Black Swan: The Impact of the Highly Improbable. Random House. Google Books [4] Taleb calls those rare, extreme-impact events that are explained away only in hindsight "black swans," arguing that they cannot be verified or predicted in advance yet often dominate the course of history. On this basis he proposes that one give up the fantasy of precise prediction and instead build arrangements that are not destroyed by surprise, and may even benefit from it. This echoes the ending of this chapter: the problem is not to abolish uncertainty, but how to live steadily within it.

← Preface: A World Without Oracles2. The Five Faces of Unverifiability →

Open with WeChat

Scan this page in WeChat, then use WeChat's share menu.