In 1976—at what seems like the dawn of the software age—my colleagues Richard Lipton, Alan Perlis, and I wrote a paper that fractured the calm surface of computer science. Social Processes and Proofs of Theorems and Programs1 was a direct, unfiltered assault on the burgeoning formal program verification movement. At the time, the software engineering community was infatuated with a seductive promise: that complex computer programs could be mathematically proven “correct,” eliminating human error and systemic unpredictability once and for all.
Looking back now, nearly half a century later, Social Processes… seems larger than a technical critique. Viewed in retrospect, our paper was a reflection on the limits of rationalism, an anti-high-modernist manifesto that anticipated the exact failure modes of today’s automated governance and laid the philosophical groundwork for resisting what I now call the Sovereign Code Doctrine.
The High-Modernist Illusion of Absolute Verifiability
We did not use the phrase “high-modernism” in 1976, but we were fighting its purest expression. As the political sociologist James C. Scott later argued in Seeing Like a State,2 high modernism is characterized by an absolute, blind faith in linear progress, standardization, and top-down rational design. The high-modernist administrator looks at complex, organic human systems and sees only messy inefficiencies to be optimized away. The high-modernist’s instinctive response is to force reality into a simplified, “legible” grid that can be centrally monitored and controlled.
The program verification movement of the late 1970s was the ultimate manifestation of this hubris within the digital realm. Its architects believed that the messy, iterative, and deeply human process of software development could be entirely flattened into a centralized grid of formal mathematical specifications. Enamored by formal methods, they presumed that a computer program could exist as a closed system of pure deductive logic, completely insulated from the chaotic variables of real-world application.
We saw this ambition as a dangerous illusion. We argued that a formal verification is not a conduit to absolute truth, because a specification complex enough to describe a real-world program is inherently either unreadable or incomplete. Even if such a specification could be imagined, it is mathematically impossible to guarantee that the code at hand represents a flawless implementation of it. The formal methodists were trying to replace the rich, localized context of software execution with a hollow, stylized caricature of mathematical perfection.
The Defense of Metis and the Open Software Society
In place of this sterile, technocratic positivism, we championed what Scott terms metis—the practical, experiential, and localized human knowledge that allows communities to adapt to unexpected anomalies. We reminded the computing world that mathematics itself does not progress through a bloodless chain of formal logic. Instead, mathematics is a social process.
A mathematical proof is accepted not because an automated oracle validates its syntax, but because it survives a grueling, communal gauntlet of peer review, debate, assimilation, modification, and historical consensus. Proof is not a mechanical derivation. It is a conversation. There is no other way to explain why among the many thousands of published proofs of theorems, an infinitesimally small fraction of them live on in the collective mathematical consciousness. A proof is an organic ecosystem of minds interacting over time. Software, by extension, derives its reliability from the same open, empirical process: it is read, tested, contested, and corrected by human beings operating within a shared culture.
This defense of the social process aligns our 1979 argument with the political epistemology of Karl Popper. In The Open Society and Its Enemies, Popper argues that absolute verification is a myth; human knowledge is fundamentally fallible, and the only protection against authoritarianism is an environment of critical rationalism where laws, ideas, and state policies remain permanently vulnerable to public challenge and falsification.
By applying this Popperian framework to computer science, we were making an early argument for an Open Software Society. We declared that code can never be accepted as an unchallengeable truth. It must remain open to human scrutiny, iteration, and rejection. The moment software is insulated from this social process, it ceases to be a tool of human reason and becomes an instrument of dogmatic authority.
The Tragedy of the Invisible Failure Mode
High-modernist architectures possess a fatal structural flaw: because their designers harbor a blind faith in the perfection of their models, they systematically dismantle the practical safeguards required to survive unanticipated errors.
We issued a stark warning regarding this psychological trap. We foresaw that a dogmatic belief in code “correctness” would breed a reckless complacency among system designers. Believing their software to be infallible, engineers would abandon the messy, defensive, and redundant safeguards—the margins of safety—that analog practitioners had relied upon for generations to recover from systemic failures.
When you engineer the human element out of a system under the guise of optimization, you do not eliminate error; you merely ensure that when the system fails, the failure mode is invisible, silent, and catastrophic. The telemetry is instantly erased, the capacity for local human intervention is stripped away, and the individuals governed by the system are left entirely defenseless.
From 1976 to the Mechanized State
The warning markers we planted out nearly fifty years ago have reached their logical destination in the modern Mechanized State. What we debated as a technical problem in software engineering has mutated into the defining constitutional crisis of our time: the rise of Sovereign Code.
Today, across the core infrastructure of public administration, from automated risk assessments in criminal justice to unauditable voting architectures in federal courts to AI-driven targeting decisions on the battlefield, tech bureaucrats deploy opaque, self-executing algorithms that make life-altering decisions without the burden of public justification. When these systems are challenged, their high-modernist defenders invoke the same defense we exposed in 1976: the architecture is too complex to inspect, too technical to reconstruct, and too optimized to be questioned by ordinary human beings.
Social Processes was a warning that absolute efficiency is a euphemism for absolute capitulation. It reminds us that our institutions are not trusted because they are mathematically correct, but because they remain permanently open to human challenge. To preserve the Republic against the encroachment of Sovereign Code, we must reclaim the core thesis of our early manifesto: we must reject the false idol of automated perfection, embrace the essential, protective friction of human messiness, and insist that no machine can ever be permitted to rule where human reason has been optimized out of existence.
Richard DeMillo/May 22, 2026/Atlanta/
- DeMillo, Richard A., Richard J. Lipton, and Alan J. Perlis. “Social Processes and Proofs of Theorems and Programs.” In Ideas That Created the Future: Classic Papers of Computer Science, edited by Harry Lewis, 447–62: MIT Press, 2021. ↩︎
- Scott, James C. Seeing Like a State: How Certain Schemes to Improve the Human Condition Have Failed. Yale University Press, 1998. ↩︎
