THEORY, PROOF, ENGINEER
Every serious engineering discipline works in this order. Software does not. The fact that doing so is considered radical tells you how wrong the field is.
THE ORDER
First, you model. You describe what the thing is, what properties it must have, what loads it must bear, what conditions it must survive. This is the theory. It exists before the artifact. It is mathematical. It can be analyzed.
Second, you verify. You demonstrate that the properties follow from the design. Not by testing an instance. By proving the general case. The structure bears the load for all configurations, not just the ones you checked. The circuit meets timing for all inputs, not just the ones you simulated. This is the proof. It is mechanizable. It is exhaustive.
Third, you build. You realize the proven design in physical material. Steel, silicon, code. The building follows the blueprint. The blueprint was verified before construction began. If the math did not work, you changed the design. Not the math.
This is how bridges are built. This is how circuits are designed. This is how control systems are specified. Model the loads. Prove the structure. Then pour the concrete.
Nobody builds a bridge and then checks whether the physics works out.
THE EXCEPTION
Software does not work this way.
The normal approach is: build the system, test it, then argue that enough testing was done.
The testing is sometimes extensive. Thousands of test cases. Coverage metrics. Fuzz testing. Property-based testing. Enormous effort to exercise the system and observe its behavior.
But testing is observation, not proof. A test says: for this input, the output was correct. It says nothing about the next input. A thousand tests say nothing about the thousand-and-first. The absence of observed failure is not the presence of demonstrated correctness.
The argument comes last. After the system is built and tested, a document is written. The document argues that the testing was sufficient. That the coverage was adequate. That the process was rigorous. That the system is therefore correct.
This is not verification. It is persuasion. The document argues. It does not prove. The reviewers are convinced or they are not. The system is correct or it is not. These two questions are unrelated.
THE REVERSAL
Occasionally, a project tries to prove an existing system correct. Build first, then prove.
The cost is always enormous. Not because proof is inherently expensive. Because the proof is reverse-engineering assurance from code that was never designed for assurance.
The code made engineering choices — mutable shared state, implicit invariants, non-obvious aliasing — that are reasonable for implementation but hostile to reasoning. The proof must account for every choice. Every alias must be tracked. Every invariant must be extracted from the code and stated explicitly. Every frame condition must be established for code that was never designed to make frame conditions clear.
This is the bridge built without analysis, then subjected to structural review after the concrete has set. The review is possible. But it requires reconstructing the engineering intent from the finished artifact. The load model that should have existed before construction must now be inferred from the structure. Every assumption that should have been explicit must now be discovered.
The cost is not the cost of proof. It is the cost of working backwards.
THE CORRECT ORDER
The correct order mirrors every other engineering discipline.
First: the mathematical model. A formal description of what the system is and what properties it must have. Not pseudocode. Not a design document. A mathematical object that can be analyzed with mathematical tools. What are the operations? What are the invariants? What are the safety properties? What must be true always, for all inputs, for all sequences of operations?
This is the theory. It exists in the language of mathematics, not in the language of implementation. It does not mention memory layouts. It does not mention allocation strategies. It does not mention performance. It describes what the system does. Not how.
Second: the proof. A machine-checked demonstration that the properties follow from the model. Not an argument. Not a review. A proof — mechanized, exhaustive, independently verifiable. The invariants hold. The safety properties follow. The model is consistent. The design is sound.
If the proof does not close, the design changes. Not the proof obligations. Not the properties. The design. This is the critical moment. This is where the order matters. In the theory-first approach, discovering that the design is flawed costs nothing. The design is a mathematical object. Changing it is free. In the build-first approach, discovering that the design is flawed costs everything. The system is already built.
Third: the implementation. A realization of the proven design in a language that compiles to executable code. The implementation carries its own verification — contracts, preconditions, postconditions, invariants — that independently check alignment with the theory. The implementation can be verified by a different tool than the one that verified the theory. Two independent checks. Two different provers. Agreement between them is evidence that is difficult to dismiss.
The theory says what. The proof says why. The implementation says how. Each is verified independently. Each can be inspected independently. The chain from mathematical property to running code is traceable and machine-checked at every link.
THE ANALOGY
A structural engineer does not build a bridge and then check whether it can bear the load.
The engineer models the load. Dead load — the weight of the bridge itself. Live load — traffic, pedestrians, snow. Dynamic load — wind, earthquakes, resonance. The model is mathematical. It exists before the bridge does.
The engineer analyzes the model. Finite element analysis. Stress distribution. Failure modes. The analysis is mechanized. It is exhaustive within the model. If the structure fails under analysis, the design changes. Steel is added. Geometry is adjusted. The span is modified. This costs nothing. It is a change to a model, not a change to a structure.
Only after the analysis confirms the design does construction begin. The construction follows the analyzed design. Inspections verify that the construction matches the design. The inspections are independent of the analysis. Two checks. One that the design is sound. One that the construction matches the design.
No one considers this radical. No one argues that structural analysis is too expensive, that it would be faster to just build the bridge and test it with trucks. No one suggests that process documentation arguing the bridge is probably fine is an acceptable substitute for structural analysis.
In bridge engineering, this is how things are done. It is not a research technique. It is not an academic exercise. It is the professional standard. The alternative — build first, then check — is called malpractice.
THE OBJECTION
The objection is always the same. Software is different.
Software is more complex than bridges. Software changes faster than bridges. Software has more states than bridges. Software operates in environments that cannot be fully modeled. Software requirements shift. Software must be delivered quickly.
Every objection is true. None is relevant.
Software is more complex — which is precisely why informal reasoning is insufficient. The more complex the system, the greater the need for mechanical verification. The human mind that cannot track the complexity is the mind that will introduce the bug. The prover that cannot close the proof is telling you the complexity is real.
Software changes faster — which is precisely why the theory should exist first. When requirements change, the theory changes. The proof is re-checked. The implementation is updated. The chain remains intact. Without the theory, a requirements change propagates through the system unpredictably. The developer changes the code. The tests are updated. The document is revised. Whether the system is still correct is anyone's guess.
Software has more states — which is precisely why testing is insufficient. The state space of a nontrivial program is effectively infinite. Testing samples this space. Proof covers it. The objection that the state space is large is an argument for proof, not against it.
Software must be delivered quickly — which is precisely why getting the design right before building matters. The cost of changing a mathematical model is zero. The cost of changing a deployed system is enormous. The discipline that seems slow — modeling before building — is the discipline that eliminates the rework that actually makes projects slow.
The objection that software is different is correct. Software is the engineering discipline that most needs formal methods and least uses them.
THE REFUSAL
Theory, proof, then engineer. It sounds obvious when you say it.
The structural engineer nods. The electrical engineer nods. The control systems engineer nods. Of course you model before you build. Of course you verify the model before you realize it. Of course you check the realization against the model. How else would you work?
The software engineer says: that is impractical. Too expensive. Too academic. Not ready for production.
The comfortable explanation is that software is a young field. Give it time. It will mature. It will converge on the same discipline that every other engineering field converges on.
This is a cop-out.
Software engineering is fifty years old. Civil engineering did not wait fifty years to start analyzing structures. It started because bridges collapsed and people died and laws were passed. Electrical engineering did not naturally evolve toward simulation. It started because circuits failed and liability attached and standards were imposed.
No engineering discipline chose rigor voluntarily. Rigor was imposed by consequences.
THE INCENTIVE
When a bridge collapses, the engineer faces criminal liability. When a building fails inspection, construction stops. When a medical device malfunctions, the manufacturer is sued. When an aircraft control system fails, the investigation is public, the findings are binding, and the responsible engineers are named.
When software fails, the license agreement says: as-is, no warranty.
This is not a maturity difference. It is a structural difference in consequences. The feedback loop that forced every other engineering discipline to adopt rigor does not exist in software. The bridge engineer who skips structural analysis faces prison. The software engineer who skips verification faces nothing.
The consequences of software failure are real — data breaches, system outages, security vulnerabilities, silent corruption. But they are diffuse. They are delayed. They are deniable. The failure is observed by users, not by regulators. The cost is borne by customers, not by engineers. The connection between the engineering choice and the eventual failure is obscured by layers of abstraction, integration, and time.
No one is accountable. So no one is careful.
THE CULTURE
Worse than the absence of consequences is the presence of an ideology that celebrates their absence.
Move fast and break things. This is not a sign of immaturity. It is a creed. The field built a professional identity around shipping speed. The engineer who delivers broken code quickly is promoted. The engineer who delivers correct code slowly is managed out. The startup that ships first wins the market. The startup that verifies first loses it.
Agile. Iterate. Ship and fix. Fail fast. These are not descriptions of a field that has not yet learned. They are prescriptions from a field that has decided not to.
The culture does not lack the knowledge that theory-first engineering is possible. The papers exist. The tools exist. The demonstrated successes exist. The culture has looked at the evidence and chosen speed anyway. Not because the evidence is unconvincing. Because the incentive structure rewards the choice.
The result is predictable. Software systems fail in ways that other engineering disciplines eliminated generations ago. Not because the solutions are unknown. Because the solutions are unprofitable.
THE TOOLS
The excuse used to be the tools.
Theorem provers required heroic expertise. Verified languages were too restrictive for real systems. There was no clean path from mathematical model to deployable code. The theory existed in one world. The code existed in another. The gap between them was crossed by hand, or not at all.
This excuse has expired.
Proof automation handles the routine cases. Verified languages compile to efficient code. The path from model to implementation, while not yet effortless, is clearly walkable. The pieces exist. The gap is closable.
The tools are ready. The field is not. And the field is not because readiness would require changing what is rewarded. The engineer who uses formal methods produces fewer features per quarter. The team that models before building ships later. The company that verifies before deploying spends money on correctness that competitors spend on features.
The tools are not the constraint. The tools have not been the constraint for years. The constraint is that correctness is not valued by the market until its absence is catastrophic, and by then the cost has been externalized to someone else.
THE QUESTION
Theory, proof, then engineer.
The order is not arbitrary. It is not a preference. It is not one approach among many. It is the order that every mature engineering discipline converges on — not through wisdom, but through consequences. Through collapses and crashes and failures that made the alternative untenable.
Software has not converged. Not because it is too young. Not because the tools are not ready. Because the consequences have not yet been severe enough, or concentrated enough, or attributable enough, to force the change.
The collapses are happening. The data breaches. The infrastructure failures. The security vulnerabilities in systems that control power grids, medical devices, financial markets, and mission critical software. The consequences are growing. The attributability is increasing. The tolerance is shrinking.
The question is not whether software will adopt the discipline that every other engineering field has adopted. The question is whether it will do so by choice or by catastrophe.
Every other field chose catastrophe. There is no evidence that software will be different.
FURTHER READING
Edsger W. Dijkstra, "On the Cruelty of Really Teaching Computing Science" (EWD 1036, 1988). The strongest statement of the position. Dijkstra argues programming is a branch of mathematics and should be taught as such. Calls software engineering "The Doomed Discipline" — doomed because it accepted as its charter "how to program if you cannot." No hedging. No comfort. The entire EWD manuscript series (over 1,100 handwritten notes, 1959–2002) is archived at the University of Texas at Austin.
Edsger W. Dijkstra, "A Discipline of Programming" (Prentice-Hall, 1976). The philosophy above, in book form. Programs derived from specifications through formal reasoning, not written and then tested. The title is precise: programming is a discipline, not a craft. The book demonstrates what that discipline looks like.
C.A.R. Hoare, "The Emperor's Old Clothes" (ACM Turing Award Lecture, 1981). A career retrospective that becomes an indictment of complexity. Contains the essential line: "There are two ways of constructing a software design: one way is to make it so simple that there are obviously no deficiencies, and the other way is to make it so complicated that there are no obvious deficiencies." Hoare watched the industry choose the second way for fifty years.
C.A.R. Hoare, "An Axiomatic Basis for Computer Programming" (Communications of the ACM, 1969). The foundation. Hoare logic — preconditions, postconditions, and inference rules for proving program correctness. Every contract-based verification system descends from this paper. Twelve pages that made formal reasoning about programs possible.
Leslie Lamport, "Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers" (Addison-Wesley, 2002). Lamport's case for specification before coding. TLA+ is a formal specification language for concurrent and distributed systems. His position: "If you're thinking without writing, you only think you're thinking." The tool enforces the discipline of making designs precise before building them.
Daniel Jackson, "Software Abstractions: Logic, Language, and Analysis" (MIT Press, revised edition 2012). Jackson's approach to lightweight formal methods through the Alloy language. The key insight: "Pick the right abstractions, and programming will flow naturally from design; pick the wrong ones, and programming will be a series of nasty surprises." Automated analysis via SAT solving gives immediate feedback on models. More pragmatic than Dijkstra, but the same underlying argument: model before you build.
---
Lingenic LLC
2026