SIE.7:9 - Consequences
Implementers receive a bounded contract that can survive technology change, and reviewers can distinguish a semantic defect from an implementation defect. Negative branches and accepted loss become testable, and optimization can proceed under a preservation predicate.
The cost is explicit rule and example work before or alongside coding. Some tools cannot represent the required branches or trace and must be wrapped, changed, or rejected for this use.