Two binaries, one law
A small fleet: an intake binary and a worker binary share one topic over a Unix socket. A fleet locus names both instances, binds their shared topic, and states a claim across the pair. Save each file under the path shown below, then run hale fleet check fleet/main.hl. The compiler derives each component artifact and checks the composition.
The shared seed names the payload and its wire subject. Both binaries and the fleet import this declaration, so the route has the same identity at every boundary.
type Task { kind: Int; body: String; }
topic Work { payload: Task; subject: "demo.work"; }The first binary: an intake that queues three tasks onto Work and connects the topic to a Unix socket. Its whole contract with the outside world is the topic declaration and the binding.
import "../shared" as t;
locus Intake {
params { queued: Int = 0; }
bus { publish t::Work; }
run() {
let mut i = 0;
while i < 3 {
t::Work <- t::Task { kind: i % 2, body: "job" };
self.queued = self.queued + 1;
i = i + 1;
}
println("intake queued ", self.queued);
}
}
main locus IntakeApp {
params { in_: Intake = Intake { }; }
bindings { t::Work: unix("/tmp/hale-fleet-demo.sock", role: connect); }
run() { }
}
fn main() { IntakeApp { }; }The second binary: a supervised executor listening on the same socket. The two programs share only the Work payload shape and the wire, with separate builds, separate processes and separate failures.
import "../shared" as t;
@supervised locus Executor {
params { done: Int = 0; }
bus { subscribe t::Work as perform; }
fn perform(t: t::Task) {
self.done = self.done + 1;
println("executor did ", t.body, " kind ", t.kind);
}
}
main locus WorkerApp {
params { ex: Executor = Executor { }; }
bindings { t::Work: unix("/tmp/hale-fleet-demo.sock", role: listen); }
on_failure(e: Executor, err: ClosureViolation) { restart(e); }
run() { }
}
fn main() { WorkerApp { }; }The fleet locus names the deployed instances, binds the topic across them, and requires a subscribed executor. hale fleet check derives the component artifacts and route from these seeds, then checks the fleet claim. The fleet itself never runs.
import "../intake" as intake;
import "../worker" as worker;
import "../shared" as t;
fleet locus Demo {
params {
producer: intake::IntakeApp;
executor: worker::WorkerApp;
}
bindings {
t::Work: unix("/tmp/hale-fleet-demo.sock");
}
claims {
every_task_has_a_worker: require subscribes(some executor, topic t::Work);
}
}$ hale fleet check fleet/main.hl
component `producer` runs `intake::IntakeApp` from intake (shape 8f334a24e69cd30c): producer-0
publishes demo.work as `t::Work`, bound unix
component `executor` runs `worker::WorkerApp` from worker (shape 3af8d329972a7088): executor-0
subscribes demo.work as `t::Work`, bound unix
route `t::Work` (demo.work, unix): producer-0 -> executor-0
ok: fleet `Demo` composed — 2 instance(s), 1 route(s), fleet_shape_hash 751c3ab9d0c76841Remove the worker subscription. The worker still typechecks on its own, but fleet verification rejects the binding because no instance receives the topic:
A worker build that quietly stopped listening. (worker/main.hl)
- bus { subscribe t::Work as perform; }
+ bus { }$ hale fleet check fleet/main.hl
binding `t::Work` wires nothing: no instance of the fleet subscribes subject `demo.work`