Correct by Construction
Build software so that correctness follows from the way it's put together, instead of trying to find and remove the bugs afterwards.
Also known as: Correctness by Construction, CbyC, CbC
Category: Software Development
Tags: software-design, software-development, software-engineering, reliability, quality, error-prevention, principles
Explanation
The usual way to get working software goes like this: write the code, test it, find bugs, fix them, repeat. Correctness gets added at the end, one bug at a time. Correct by Construction takes the opposite route. You design the program so that whole categories of bugs can't appear in the first place.
The idea goes back to Edsger Dijkstra. In his 1972 Turing Award lecture, "The Humble Programmer", he argued that you should not first write a program and then prove it correct. Instead: "the programmer should let correctness proof and program grow hand in hand." Later, Praxis High Integrity Systems (in the UK) turned that idea into an industrial method for safety-critical and secure systems, using formal specifications and the SPARK language.
**Why does this matter?**
Testing shows the presence of bugs, never their absence (Dijkstra again). You can't test every input. But you can make some mistakes impossible. Every bug you rule out by construction is a bug you never need to test for, debug or patch in production.
**What it looks like in everyday code**:
You don't need formal proofs to apply the spirit of it. Most of the principles around the Pit of Success are correct by construction at a smaller scale:
- **Types that rule out invalid data**: invalid states can't be written (see Make Illegal States Unrepresentable)
- **Smart constructors**: the only way to create a value checks its rules, so every instance is valid
- **Parsing at the boundary**: untrusted input becomes precise types once, and the core never sees raw data (see Parse, Don't Validate)
- **Total functions**: every input gets an answer, so there's no hidden crash path
- **Safe APIs**: parameterized queries make SQL injection impossible to write by accident
- **Memory-safe languages**: buffer overflows and use-after-free bugs disappear as a class
**At the formal end of the spectrum**:
- **Formal specifications** written before the code
- **Refinement**: turning the specification into code step by step, with each step proven correct
- **Verified languages and tools** like SPARK, Dafny, Coq or Lean, where the compiler checks proofs alongside the code
**Correct by Construction vs. testing**:
The two aren't enemies. Construction removes the bugs that design can rule out. Tests (unit tests, property-based tests) then cover the behavior that types and structure can't express. The more you shift into construction, the smaller and more focused your test suite can be.
**Keep in mind**:
Full formal verification is expensive, and most projects don't need it. The practical move is to pick the bugs that hurt the most (security holes, data corruption, crashes) and make those impossible by design. Test the rest.
Related Concepts
← Back to all concepts