Structural Correctness
"Structural Correctness" (SC) is introduced as a formal property for verifying that a system's internal data structures, invariants, and state transitions are correctly implemented. It offers a practical middle ground between full specification and no verification, ensuring data integrity without dictating complete system behavior.
Background
- The author, SAO (a pseudonym), writes about software engineering and systems design. This post introduces "structural correctness" — a concept that bridges formal program verification (mathematical proofs that code behaves as specified) and practical engineering.
- Traditional "correctness" in computer science means proving a program's behavior exactly matches its spec. This is rigorous but costly and brittle. "Structural correctness" proposes a middle ground: architecting systems so that correct behavior emerges naturally from their structure, without full formal proof.
- The piece draws on programming language theory (types, compilers), distributed systems, and common engineering patterns. The argument: getting the structure right — how components fit together and what guarantees they offer — is more practical than proving everything formally.
- This matters because modern software is enormously complex. Formal verification (used in avionics, for example) is too expensive for most projects. Testing alone leaves gaps. Structural correctness offers a pragmatic framework: design systems that make it hard to be wrong by accident.