2,376 Years
Originally published on Substack.
A reporter once asked Einstein if he could recite the speed of light from memory. Einstein said he could not, and did not intend to. That information is available in any physics textbook. Why would I clutter my mind with facts I can look up in two minutes? What matters is the ability to think.
He was not being modest. He was making a claim about where intelligence lives. Not in the accumulation of formulas, but in the capacity to reason with them.
For most of history, the textbook was a dead object. You had to carry the reasoning yourself. The book held the formula. Your mind had to apply it.
That distinction has collapsed.
In 350 BCE, Aristotle wrote down the rules of valid inference. If all men are mortal, and Socrates is a man, then Socrates is mortal. Not as a fact about Socrates, but as a structural fact about the argument itself. The conclusion follows necessarily from the premises. The form is what matters.
This was the first piece.
He could not have known he was starting something that would take 2,376 years to finish.
The Pieces
Leibniz, working in the late 1600s, had a vision he called the calculus ratiocinator: a symbolic language in which all disputes could be resolved by calculation. When two philosophers disagreed, they would not argue. They would say let us calculate and sit down with their symbols. He spent years designing the notation. He could not build the engine that would run it. He died with the vision intact and the machinery missing.
Boole, in 1854, completed the algebra Leibniz imagined. Logical statements (AND, OR, NOT) could be manipulated like numbers. Thought had an arithmetic. He built a beautiful calculus. He could not automate it. The calculation still required a human to perform it.
Frege, in 1879, built the first formal logical system powerful enough to represent mathematical reasoning. Predicate logic, quantifiers, the full apparatus. He thought he had finished the job. Russell showed him a paradox that made the whole system collapse. Frege revised his work until the end of his life. He said in his diary, near the end, that the foundation had shaken under him.
Russell and Whitehead spent ten years writing Principia Mathematica, 2,000 pages proving that 1+1=2 from first principles. The proof of 1+1=2 appears on page 379. They were not joking. They were building the foundation. The foundation was real. And it was still entirely manual.
Church and Turing, independently and within months of each other in 1936, formally defined what it means for something to be computable. Church with his lambda calculus. Turing with his imaginary machine. Between them they gave computation its mathematics. Programs were not yet a thing. The theory was older than the practice.
Hoare, in 1969, gave us the contract. If you state what must be true before a function runs (the precondition) and what must be true after (the postcondition), then the implementation can be checked against those promises. Programs could now be argued about the way mathematics is argued about. A proof of correctness, not just a test.
Milner, through the 1970s and 1980s, built type theory to the point where whole categories of error became structurally impossible. Not caught by tests. Not prevented by discipline. Impossible to express. A well-typed program cannot have certain bugs the way a circle cannot have corners. The error is not there to find because it was never allowed to form.
Girard, in 1987, found something stranger: a logic for resources. Linear logic. The ability to say that something must be used exactly once. Not zero times, not twice, once. A ticket that cannot be copied. A key that is consumed when the lock opens. This was not just aesthetics. It was a new kind of guarantee.
Honda, in the 1990s, developed session types: the ability to encode a protocol as a type. If process A and process B are communicating, the type system can guarantee they are always in compatible states. No deadlock by structural impossibility. No protocol violation because the violation cannot be typed.
Denning, in 1976, developed information flow analysis: the ability to prove that sensitive data can only travel along permitted paths. Not by auditing every line of code for leaks. By making unauthorized flows impossible to express in the type system. Security as geometry rather than inspection.
Every one of these was a genuine breakthrough. A new piece added to the machinery. And the machinery never deployed.
Why the Machinery Never Deployed
Each breakthrough came with a cost: you had to understand it to use it.
Hoare contracts require you to state the preconditions correctly. If you state them wrong, if you describe the territory imprecisely, the contract fails silently or (worse) proves something you did not intend. You need to know what a well-formed precondition looks like. You need to know the theory.
Milner types require you to annotate the code correctly, to understand what the type system is checking and why. A type error is a compressed formal argument, and reading it requires fluency in the language of types.
Girard’s linear types require you to reason about consumption in a way that goes against every ordinary programming habit. The concept is not hard in the abstract. Applying it consistently to a real program requires a particular kind of training.
Session types and information flow analysis require more still. They require you to have read the papers. Not skimmed. Read. Understood the formal apparatus. Can apply it under pressure, in a codebase you did not write, with requirements that keep changing.
The annotation burden was not recoverable at human scale. You could deploy these tools in a small number of places (aircraft navigation software, pacemaker firmware, nuclear control systems) where the cost of the annotation was justified by the cost of failure.
For everything else (the small business inventory tool, the scheduling script, the game an engineer builds for her daughter on a Saturday) the cost was simply too high. The machinery sat waiting.
2,376 years. Piece after piece added to the engine. The engine never started.
2026
The AI assistant has read the papers.
Not metaphorically. These systems trained on the entire formal methods corpus. Every implementation of Hoare logic, every paper on linear types and session types, every example of information flow analysis ever published. They have internalized the patterns at a depth that makes them applicable without the practitioner needing to understand the underlying theory.
The annotation burden (the thing that kept the machinery from starting) was the cost of learning the theory and applying it correctly by hand. That cost has moved.
What the AI is missing is not the theory. It has the theory. What it is missing is your system. It does not know what your invariants are, what your protocols mean, what resources in your domain must be consumed exactly once and which can be shared. Every session starts from scratch.
A specification closes that gap.
Write a precise description of what your system must be. Name the territory. What a record is, what a transaction means, what must never be allowed to happen. Not code. Not implementation. The domain, stated clearly.
The AI reads that specification and applies 2,376 years of accumulated machinery to it. Hoare’s postconditions, automatically. Milner’s type safety, automatically. Girard’s resource tracking where the domain calls for it. Session protocol checking where processes communicate. Information flow guarantees where data must be confined.
You did not need to read the papers. You named the territory. The machinery engaged.
What 2,376 Years Adds Up To
It adds up to this: every formal idea that ever prevented a program from being wrong is now available to every practitioner who can describe what they want clearly enough for the machinery to engage.
Not for aircraft. Not for pacemakers. For everything.
The inventory tool for the small shop. The scheduling script for the sports league. The flea game an engineer builds for her daughter on a weekend. All of them can now have the structural guarantees that Aristotle made possible in 350 BCE, that 2,376 years of mathematics progressively refined, and that for most of that time no one could actually use on a Saturday afternoon project.
The Aristotle who wrote down the rules of valid inference did not know he was building the first component of something. He was just trying to understand how arguments work. Leibniz did not know he was building the second component. He was just trying to mechanize reasoning. Hoare, Milner, Girard, Honda, Denning. Each one added a piece to a machine whose purpose they could see only partially.
The purpose is clearer now.
A practitioner sits down with her domain (her fleas, her platforms, her invariants) and describes what the system must be. The machinery that took 2,376 years to build is waiting on the other side of that description.
Einstein was right. What matters is not the formula in your head. It is the ability to think.
The textbook is no longer dead. It holds not just formulas but the accumulated reasoning of 2,376 years. And it knows how to apply that reasoning to new situations. What remains irreducibly human is exactly what Einstein said: the thinking. The ability to look at your domain and say precisely what it is.
That is the specification.
That is all it has ever needed to be.
Generative Specification is a discipline for building software with AI assistance that produces consistent, auditable, formally grounded results. The white paper, the field guide, and the tools are open access at pragmaworks.dev.