Claim-Driven Development in Hale /articles Article 4 August 2026 v0.14.0<br>Claim-Driven Development in Hale<br>The effects system lets one function make a promise.
A handler can say that it never blocks. A computation can say that it never<br>reads the clock. A locus can say that nothing arriving through the bus may<br>transitively cause a payment. The compiler follows calls and message edges and<br>either proves the assertion or returns the path that violates it.
Some requirements do not belong to one function.
the Delta side of an organization must never enter the Gamma side
nothing in one tenant may reach another tenant’s knowledge
exactly one component may publish settlement commands
every task vocabulary must have a handler
every path to the ledger must pass through authorization
processing one task may invoke the model at most once
Those are laws of the assembled system.
Spreading them across function annotations would make completeness depend on<br>remembering every entry point. The requirement itself would still have no<br>single name, no single location, and no source line a reviewer could identify<br>as the place where the law changed.
Hale’s claims system gives those requirements a place to live.
A claim is a named sentence over the program graph . It is evaluated by<br>hale check and lowers to no runtime code. If it is false, the compiler returns<br>a counterexample: a path, an ungranted boundary edge, an uncovered topic, a set<br>of competing writers, or an excessive capability count.
That enables a development style with a deliberately literal name:
Claim-driven development writes the system’s law first, then changes the<br>program until the compiler can prove it.
The loop works today without a synthesizer:
state the claim
hale check
countermodel or missing obligation
edit the program
hale check
An idea being explored for later is hale next: ask the compiler to propose<br>the next legal construction or smallest repair. But that command is not what<br>makes the workflow claim-driven. The essential loop already exists whenever a<br>failed claim identifies what the program must do—or stop doing—next.
Effects say what a piece of code may do.
Claims say what must remain true of the whole.
Write the law before the wiring
Most architecture work is implementation-first.
You create components, add calls, wire topics, choose placement, and eventually<br>inspect the resulting system to see whether the intended boundaries survived.<br>Tests and review then try to reconstruct the architecture from the completed<br>program.
Claim-driven development reverses a narrow but important part of that order.
Start with a skeleton whose important declarations exist. Name the domains.<br>Write what must be absent, what must be present, and what must be unique. Then<br>let the compiler reject incomplete and malformed arrangements while the system<br>is being assembled.
Consider an application shared by two semi-independent organizations.
Delta receives work and performs triage. Gamma performs research. Each side has<br>its own store. Both may call an external model. Gamma is allowed to send one<br>research digest to Delta, but Delta must never enter Gamma’s executable domain<br>or read Gamma’s knowledge.
The project might be organized as:
lib/topics/ shared topics and effect vocabulary
delta/ Delta positions and store
gamma/ Gamma positions and store
app/main.hl the assembled organization and its law
Before the implementation is complete, main.hl can already name the domains:
group delta_wing = { delta::* };
group gamma_wing = { gamma::* };
group positions = {
delta::DeltaTriage,
gamma::Research
};
group gateways = {
GithubGateway
};
And the main locus can state the first version of the law:
main locus Org {
params {
github: GithubGateway = GithubGateway { };
triage: delta::DeltaTriage = delta::DeltaTriage { };
research: gamma::Research = gamma::Research { };
claims {
delta_does_not_enter_gamma:
forbid reaches(delta_wing, gamma_wing);
tasks_are_consumed:
require subscribes(
some delta_wing,
topic t::Tasks
);
one_task_ingress:
count publishers(topic t::Tasks) == 1;
Suppose the gateway publishes Tasks, but DeltaTriage does not yet subscribe.
The program is incomplete, and the claim says exactly how:
claim `tasks_are_consumed` violated:
no member of `delta_wing` subscribes `t::Tasks`
Add the missing declaration:
locus DeltaTriage {
bus {
subscribe t::Tasks as on_task;
fn on_task(task: t::Task) {
// implementation still in progress
Run hale check again.
The missing obligation is satisfied. The negative boundary claim remains in<br>force while the handler is filled in. Later, if a helper call or message route<br>crosses into Gamma, the same check becomes red again.
This is the basic development loop:
positive claims prevent an empty system from appearing complete
negative claims prevent implementation from escaping its boundaries
exact claims prevent accidental multiplicity
quantitative claims prevent permitted behavior...