03 · Epistemology

Part I's third hearing: having asked what a program is, the court now asks what it is entitled to claim it knows.

Does a machine's answer count as knowledge?

In 1976, Kenneth Appel and Wolfgang Haken, at the University of Illinois at Urbana–Champaign, announced a proof of the four-color theorem — the claim, open since 1852, that any map can be colored with four colors so that no two adjacent regions share one. Their method reduced the infinite variety of possible maps to an unavoidable set of 1,476 configurations, each of which had to be checked for "reducibility" by machine; the computer ran roughly 1,200 hours (Robertson, Sanders, Seymour & Thomas, "The Four Color Theorem"). No mathematician has ever read that check line by line, and none ever will; the case-work is too vast, and no journal referee re-derives it. The result was the first proof of a major theorem that essentially required a computer, and it unsettled mathematicians precisely because it broke an assumption so old it had never needed stating: that a proof is something a trained human being can, in principle, follow from first line to last and certify with their own understanding. The four-color theorem is almost certainly true. Whether the Appel–Haken argument counts as a proof in the older sense — something surveyable, something a mind can hold — is a question the mathematical community has never fully closed.

That unease is this chapter's opening exhibit, and it names the first principle directly: surveyability is not guaranteed, and its loss changes what proof can do for us. Descartes's classical picture of mathematical certainty assumed a chain of steps small enough, and clear enough, for one mind to inspect every link. Appel and Haken's proof is sound by every formal standard computer scientists can specify, yet it asks for a different kind of trust — trust that the compiler compiled correctly, that the hardware did not glitch across 1,200 hours, that the case-generating program itself contained no error. The theorem may be certain; the route to believing it has become an engineering claim as much as a logical one.

The second principle addresses a method that never pretended to surveyability in the first place: simulation. Paul Humphreys and, at greater length, Eric Winsberg (Science in the Age of Computer Simulation, University of Chicago Press, 2010) have argued that computer simulation supplies neither classical empirical evidence (you cannot rerun Earth's actual climate as a controlled experiment) nor classical theoretical deduction (a climate model is stitched from theory, numerical approximations, and hand-tuned parameters no single equation justifies). Winsberg calls this a distinct epistemic category: trust in a simulation rests on trust in the model's construction — the physics it encodes, the tricks it uses to make intractable equations tractable, the track record of similar models on cases you can check — rather than on trust that the modeled object and the real object are, in the experimenter's sense, "the same kind of system." A hurricane-track simulation is neither an observation of a hurricane nor a proof about one; it is a third thing, evidence built rather than found.

The third principle is opacity, and it cuts a line straight through modern computing. Humphreys coined "epistemic opacity" for processes in which not all the elements relevant to a result's justification are, even in principle, available to the epistemic agent making use of it (Extending Ourselves: Computational Science, Empiricism, and Scientific Method, Oxford University Press, 2004). A traditionally written program is transparent in a specific sense: however long, its logic is in principle inspectable, line by line, by a competent reader. A trained neural network is opaque in a different sense: its "reasons" are distributed across millions or billions of weighted connections that were never designed, only grown by gradient descent, and no human — not even its authors — can trace why one output rather than another emerged. This bears directly on machine testimony: when a diagnostic model flags a tumor, is that a report from a reasoning entity, to be weighed the way we weigh a colleague's judgment, or a reading, to be weighed the way we weigh a thermometer's? The two carry different epistemic weight, and opaque systems make it uncomfortably hard to tell which one you are getting.

The fourth principle replays an old civil war under new names: program verification versus testing, rationalism versus empiricism. In May 1979, Richard De Millo, Richard Lipton, and Alan Perlis published "Social Processes and Proofs of Theorems and Programs" (Communications of the ACM 22, no. 5: 271–280), arguing that mathematical certainty rests on a social process — peers checking, re-deriving, and eventually trusting a proof — that program verification could never replicate at scale, because no comparable community will re-verify a million-line formal proof of a shipped product. James Fetzer's 1988 "Program Verification: The Very Idea" (Communications of the ACM 31, no. 9: 1048–1063) sharpened the objection into a philosophical claim: algorithms, as abstract logical structures, admit deductive proof; programs, as physical processes running on real, occasionally faulty hardware, do not, because no deduction can certify that silicon will behave as its specification assumes. The verificationist's rationalist ideal — prove it once, know it forever — meets the tester's empiricist reply, distilled by Edsger Dijkstra a decade earlier: "Program testing can be used to show the presence of bugs, but never to show their absence" ("Notes on Structured Programming," EWD249, 1970). Neither side has won; software ships today on some blend of both, verified where it is cheap enough, tested everywhere else.

The fifth principle is the oldest trap in epistemology, wearing a sensor's housing. Edmund Gettier's three-page 1963 paper, "Is Justified True Belief Knowledge?" (Analysis 23, no. 6: 121–123), showed that a belief can be justified and true and still fail to be knowledge, when the justification and the truth connect only by luck — the classic image is a stopped clock that happens to show the correct time. Automated pipelines manufacture this structure routinely: a facial-recognition system with a genuine bug — miscalibrated, say, on faces at a certain angle — can still output the correct match on a given frame, by accident, while carrying all the institutional justification ("this system is 99% accurate") that would normally certify a belief as knowledge. The output is true, and reasonably trusted, and arrived at by a process that, on that occasion, was not doing what its justification assumed it was doing. Gettier's stopped clock now has cameras.

The people, briefly. Appel and Haken took considerable heat for a proof many still call inelegant rather than false. Humphreys and Winsberg built an entire subfield — the philosophy of computer simulation — out of taking seriously a method working scientists had already trusted for decades without asking what kind of evidence it was. Fetzer's 1988 paper triggered pages of technical correspondence within a year and a debate still cited today — one of the longest-running controversies Communications of the ACM ever printed.

Connections

Chapter 01 supplies the proof-theoretic background — soundness, completeness, and Gödel's limits — that surveyability quietly assumes. Chapter 09 asks what undecidability licenses philosophically, a companion question to what unsurveyable proof licenses here. Chapter 13 returns to opacity from the learning side: interpretability research as a laboratory for finding out what, if anything, is inside the black box.

Open questions

If a proof can be certain but not surveyable, has "proof" quietly changed meaning since Euclid, or did it always mean "warranted to the standards of the day" and Euclid's standards were simply stricter than ours by accident of history? And is machine opacity a temporary engineering limitation interpretability research will eventually dissolve, or a permanent structural feature of any system whose "knowledge" is distributed statistically rather than written down as rules?

Go deeper

• Eric Winsberg, Science in the Age of Computer Simulation, University of Chicago Press, 2010 — the founding case for simulation as its own epistemic category.
• Richard A. De Millo, Richard J. Lipton, and Alan J. Perlis, "Social Processes and Proofs of Theorems and Programs," Communications of the ACM 22, no. 5 (1979): 271–280; James H. Fetzer, "Program Verification: The Very Idea," Communications of the ACM 31, no. 9 (1988): 1048–1063.
• Computer Simulations in Science, Stanford Encyclopedia of Philosophy.