# The check comes first

> A check is proven before it is trusted, as shown in the order]. The proof has two halves, and each catches a failure the other cannot.

Page: Methodology · Build
Canonical: https://banes-lab.com/disciplined-methodology/build#the-check-comes-first

This section is stop 33 of 102 in the learning route. Previous: [18 - The gate holds the line](https://banes-lab.com/disciplined-methodology/build/the-gate-holds-the-line.md). Next: [20 - A check matches a shape](https://banes-lab.com/disciplined-methodology/build/a-check-matches-a-shape.md). It builds on [18 - The gate holds the line](https://banes-lab.com/disciplined-methodology/build/the-gate-holds-the-line.md).

A check is proven before it is trusted, as shown in [C1·a the order](https://banes-lab.com/disciplined-methodology/build#the-check-comes-first-panel-a). The proof has two halves, and each catches a failure the other cannot. The same discipline applied to checks that already exist is described in [verify the verifier](https://banes-lab.com/disciplined-methodology/verify/verify-the-verifier.md).

### Check, prove, then build

A check written after the code describes the code rather than the rule. The check comes last and passes on its first run, and neither you nor the model ever learns that it would have passed anything. A check has only the code in front of it to be shaped by, so it learns the code's accidents as the rule; [testability](https://banes-lab.com/records/arch/testability.md) is either designed in or absent.

For this reason the check comes before the code, and I trust a check only after it has caught something on purpose and let something through on purpose. Every change is ordered as check, planted violation, conforming member, then code, rather than code first with a check fitted around it. In practice, the check is written first, then broken on purpose to see that it fires with the expected message. It is then run over the real population to confirm that at least one real member passes for the right reason. The planted file is restored, and only then is the code the check will hold written. After a check is narrowed for precision, the case that motivated it is run again.

To check this, find the change where each check first fired and the member it first cleared. A check with no such moments has never shown that it works. A check that every member satisfies for free always says the same thing, and its green result then passes for evidence that what it measures is working. Where nothing can disagree with a check, it is kept with the property it cannot test written down, rather than shipped in a weaker form.

The two halves of the proof answer two different questions. A planted violation shows that the check can reject, because a check that has never been seen to fail looks the same as one that cannot fail. A real member passing shows that the check can tell members apart. A check that every member fails has only been shown to reject, and its first green result looks the same as a scope that stopped reaching anything, the [mock mirage](https://banes-lab.com/records/arch/mock-mirage.md) of a test that exercises nothing real. Where no member can pass yet because the correct shape does not exist in the tree, the first conforming member is written beside the check in the same change, and the check is proven against it before either is trusted.

Narrowing is where a correct check can lose its subject without anything reporting it, and it is where the rule in [a check matches a shape](https://banes-lab.com/disciplined-methodology/build/a-check-matches-a-shape.md) is easiest to break. A rule is written against one case and then scoped for precision. Each refinement is judged by the false positives it removes, and neither the developer nor the model runs the true positive again, so a scope that excludes the motivating case reads exactly like a scope that got tighter. The cheapest scoping is the harmful one, because it keys on the property the correct members share rather than on the property the defect has. Running the motivating case again after every scoping costs a sentence, and it is the only step that tells a check that became precise from one that became blind.

C1·a the order

```mermaid
flowchart TB
write["Write the check"]
plant["Plant a violation"]
fires{"Does it report the expected message?"}
real["Run it over the real population"]
passes{"Does at least one real member pass for the right reason?"}
restore["Restore the planted file"]
code["Write the code the check holds"]
write --> plant --> fires
fires -- no --> write
fires -- yes --> real --> passes
passes -- no, everything fails --> write
passes -- yes --> restore --> code
```

## Links to

- [Verify the verifier](https://banes-lab.com/disciplined-methodology/verify/verify-the-verifier.md)
- [Testability](https://banes-lab.com/records/arch/testability.md)
- [Mock Mirage](https://banes-lab.com/records/arch/mock-mirage.md)
- [A check matches a shape](https://banes-lab.com/disciplined-methodology/build/a-check-matches-a-shape.md)

## Linked from

- [Algorithm examples](https://banes-lab.com/pag/patterns/algorithm-examples.md)
- [Verify the verifier](https://banes-lab.com/disciplined-methodology/verify/verify-the-verifier.md)
- [Coverage is derived](https://banes-lab.com/disciplined-methodology/verify/coverage-is-derived.md)
- [A cell that resists an invariant](https://banes-lab.com/software-architecture/coverage/a-cell-that-resists-an-invariant.md)