What a Hale program describes

A type is data. A locus is anything that lives.

A type is shape. A locus is anything that owns state or takes part in flow: an application, a service, a connection, a worker, a cache, a pipeline stage, an adapter. Anyone who knows actors, or services that only talk over queues, knows most of it already; the rest of this page is what the compiler can do once nothing else exists. Each locus has a parent, may own children, and owns a memory region. The ownership tree is therefore also the lifetime tree and the failure tree. A locus that dissolves takes what it owns with it.

Three graphs, and the compiler knows how they meet

Most stacks spread those three across source, runtime libraries, broker configuration and deployment manifests. Hale keeps them separate enough to reason about and joined enough for one checker to walk all three. The compiler will draw them. The communication graph of a four-locus program follows, rendered by hale topology graph from the build artifact.

Change one line so a value passes through a function-typed parameter, and the graph grows a vertex that is not part of the program.

A topic names the edge and says nothing about the mechanism

A topic is a typed, named edge. A publisher declares the authority to send; a subscriber declares the handler that receives. No channel handle or broker client is threaded through constructors.

topic Reading { payload: Sample; }

locus Ingest {
    bus { publish Reading; }

    fn received(s: Sample) {
        Reading <- s;
    }
}

locus Rollup {
    bus { subscribe Reading as add; }

    fn add(s: Sample) {
        // owns the rolling state
    }
}

A closed-world local edge may lower to a direct call. Other local edges use the bus. A binding can carry the same topic over a socket, shared memory, UDP, or an adapter you wrote.

main is the architectural linker

Domain loci say what the system is. main says where its parts run and how its topic edges travel. A test can omit bindings; production can split the same source across processes.

main locus App {
    params {
        ingest: Ingest = Ingest { };
        rollup: Rollup = Rollup { };
    }

    placement {
        ingest: pinned(core = 1);
        rollup: cooperative(pool = compute);
    }

    bindings {
        Reading: unix("/run/readings.sock", role: listen);
    }
}

Effects include causality

Hale can constrain blocking, allocation, syscalls, time, entropy, publication, spawning and recursion across a reachable call path. Causality is an effect because it follows the same rule as the rest: a property is declared at one site and proven over everything that site can reach, and reaching does not stop where the call stack does. A function that publishes has handed its influence to whoever subscribes, and to whoever they publish to in turn. A declared dependency set says which subjects may arrive at the end of that chain, and the compiler walks it. See it reject one, or read the witness it hands back.

The law keeps going past the executable

Effects close around a function. Claims close around one assembled application. Neither can say anything about the entry point next door, or about the arrangement of binaries you actually deploy. The structure continues, and the same checker follows it.

A constitution is a claimset written once and adopted per entry point. Every clause is still evaluated in the adopting main's own closed world: one text, many worlds, many independent verdicts. Composition is by union only, so a derived constitution can add a rule and cannot replace one. Which law applies is a property of where you deploy, so the binding lives in hale.toml, and hale check --matrix proves every entry point against every environment that runs it. An entry point listed in no environment is an error.

A fleet is one scale further out. Each application emits a byte-reproducible topology artifact. A plan names deployed instances and the routes between them. hale fleet check composes those artifacts, never merged source, and proves law no single binary can state. Matching topic declarations connect nothing; only an explicit route creates an edge, because an unbound topic is in-process by default and merging source would invent edges no deployment has. Signatures over the artifact's exact bytes, and per-instance binary digests, carry the certificate to the machine that runs it.

A plan carries instances, routes, groups and claims, so it plays the role of a main locus one scale out, over separately compiled binaries. The plan composes certified artifacts and is itself JSON; Hale source has no fleet syntax. What recurs is the model.

Two axes

This page climbs one axis and the guide climbs another. Scale is how large the composed system is, from function scope to fleet. Altitude is how much of the machinery you choose to control, from everyday code to explicit systems work. They are independent: one locus takes part at every scale while being written at whichever altitude the job needs, which is why the guide can teach a script before it teaches placement without leaving this model.

The commitments

• Nothing stateful is ownerless

  State and lifetime have a structural home.

• No edge is ambient

  Every communication edge is named, typed and authorized.

• Behaviour can be surfaced

  Blocking, allocation, publication and dependence can become contracts.

• Failure goes somewhere structural

  Recovery belongs to an owner with context.

• Deployment is part of the program

  Placement and transport are declared in the program.

• Unknown is not proven

  A hard guarantee fails closed at a certification boundary. Ordinary hale check still reports some topology findings as advisories; hale verify, a contract or a claim turns not knowing into a failure.

• Runtime change crosses declared seams

  Dynamism moves between valid arrangements.

Where it stands

Each stage hands evidence to the next.

That is the model you write. The one the compiler derives from it, the typed value behind claims, artifacts, fleet composition and lowering, is the semantic model, which ends at the contract itself in spec/model.md.