Correct by Construction

Correct by Construction (CbC) is a programming methodology where the proof of correctness of the program is developed with the program, as opposed to post-hoc verification where correctness is proved after implementation. For example, the idea of weakest-precondition calculus developed by Dijkstra and later Gries, derives a program backwards from its postcondition, the derivation yielding both the program and the precondition under which it establishes that postcondition . A separate tradition applies the idea to dependently typed languages (like Rocq). The Curry–Howard correspondence gives a direct relationship between typed computer programs and constructive mathematical proofs. It identifies types with propositions and well-typed terms with proofs. Because dependent types may refer to values, a type can express a full specification, and a term inhabiting it is both the program and the proof that it meets the specification. Here, correctness is proved by typechecking rather than by a separate proof.

From a software engineering perspective, Correct by Construction emphasises correctness at the lowest levels of code and algorithmic design to reduce cycle time and cost, improve product quality, and allow real-time product feedback.

Principle

Design errors are often discovered late in the development cycle or after release, and bugs that escape verification are costly and time-consuming to fix. The aim of CbC is to catch and eliminate as many defects as possible early, before designers enter register-transfer level (RTL) design and before verification engineers write testbenches in a hardware verification language.

For example, in civil engineering, a bridge designer first creates an accurate computer model of the proposed solution before laying the foundations. Similarly, CbC model is used to reason about the proposal and to ensure that required functionality is delivered and correct behaviour exhibited.