Principles

The meaning of a thing is what it is, what it may become and what may be done with it.

1. 1.11 The conditions a thing can be in are its states. What may be done with it are its operations, and which are allowed depends on its state.

Software is built by composition.

1. 1.21 Composition joins parts, each with a meaning of its own.
2. 1.22 Some parts provide capabilities. Others hold the rules of a domain.
3. 1.23 Capabilities recur from product to product. A domain belongs to one.

Every part carries assumptions about data, effects and failure.

1. 1.31 An effect is whatever a part does to the world beyond it.
2. 1.32 Where those assumptions differ, integration work begins.
3. 1.33 Where they differ only by convention, translating between them adds cost and nothing else.

The cost of software lies as much in the joins as in the parts.

Whoever writes the code makes the guess.

1. 2.11 Two reasonable guesses can contradict each other.
2. 2.12 Software built on contradicting guesses breaks at its joins.

An agent is a model that writes code. It changes what code costs, not what code must do.

1. 2.21 When code is cheap, guesses multiply.

An agent builds on the foundation it is given: the parts, conventions and language around it.

1. 2.31 An agent inherits that foundation's strengths and its omissions alike.
2. 2.32 Whatever a foundation permits, an agent will eventually write.
3. 2.33 A foundation and the software built on it form one system.

Mistakes are certain. Their kinds are not.

1. 2.41 A foundation decides which kinds are prevented, which are exposed and which get through.

A review is a judgement, not a proof.

1. 2.51 People decide what software must mean.
2. 2.52 A choice the meaning did not make is meaning still to be decided.

Software is correct when it does what its meaning says.

1. 3.11 Correctness can be judged only against meaning that is stated.

An instruction can be ignored. A check cannot.

1. 3.21 A check verifies a property by machine, on every change.
2. 3.22 A rule nothing checks will be broken, given enough changes.

An ontology makes meaning explicit: what each thing is, and how each relates to the rest.

1. 3.31 One ontology is shared by all who build.
2. 3.32 An ontology nothing checks is only a description.
3. 3.33 Meaning that is stated and checked is a boundary.

Every state a thing can take must be named.

1. 3.41 An unnamed state is handled by accident, or not at all.

External input is untrusted until it is validated.

1. 3.51 Data is validated once, where it enters.

A part may cause only the effects it is given.

1. 3.61 What is given can be replaced: a part can be tested without the world it touches.

Types describe the states data can take and the operations allowed on it.

1. 4.11 When types name every state, a forgotten case is found before the code runs.
2. 4.12 Types draw boundaries no code can cross.
3. 4.13 Invalid states must be unrepresentable.
4. 4.14 Once validated, data carries what was checked in its type.
5. 4.15 Not every rule of a domain fits in a type. Every rule that fits belongs there.

Code must state plainly what it means to do.

1. 4.21 A person can judge only what the code makes plain.

A language is one layer of a foundation, not the whole of it.

1. 4.31 No language makes software correct on its own.
2. 4.32 Types rule out classes of error, not errors of logic.

What types cannot rule out must be tested.

1. 4.41 Tests challenge behaviour. A passing test shows a case that works, not that none fails.
2. 4.42 A test written from the meaning challenges the code. A test written from the code repeats its assumptions.

What tests cannot settle must be observed.

1. 4.51 Load, timing and the real shape of data are known only in operation.

Reliability comes in layers, not from any single mechanism.

1. 4.61 Each layer catches errors the one before it lets through.

Coherent conventions reduce arbitrary choices.

1. 5.11 Every arbitrary choice is a chance to be wrong.

Parts designed together compose without translation.

1. 5.21 Data, effects and failure are modelled one way across every part.

One canonical approach is worth more than several good ones.

Tests that travel with a part preserve what was learned in building it.

1. 5.41 A foundation is trusted when its parts are tested together.

Every part says how it is meant to be used.

1. 5.51 Its types turn that statement into a check.

Composition comes before invention.

1. 6.11 A part that already exists need not be guessed again.
2. 6.12 New code is written for the rules of a domain.

Deterministic where possible. Intelligent where necessary.

1. 6.21 Mechanical work is done by machines, the same way every time.
2. 6.22 An agent is asked only where judgement is needed.
3. 6.23 Where generated code and an agent's code meet, a check decides whether they fit.