Programs used to describe computations. Hale describes running systems.

Ownership, lifetime, concurrency, communication, supervision, and deployment are usually documented in different languages. Hale treats them as views of one program.

The locus is the situated part of the program

A type is data. A locus is anything that owns state or participates in flow: an application, service, connection, worker, cache, pipeline stage, or adapter.

Each locus has a parent, may own children, and owns a memory region. The ownership tree is therefore also a lifetime and failure tree. When a locus dissolves, its owned structure dissolves with it.

There are three graphs, and Hale knows how they meet

Most stacks scatter those graphs across source code, runtime libraries, broker configuration, and deployment manifests. Hale keeps them separate enough to reason about and joined enough for the compiler to check.

You do not have to take that on faith. The compiler will draw them. Here is the communication graph of a four-locus program, rendered by hale topology graph from the build artifact — not a diagram anyone maintained:

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:

Topics describe communication without smuggling in a mechanism

A topic is a typed, named edge. Publishers declare authority to send; subscribers declare 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 a user-written adapter.

main locus is the architectural linker

Domain loci say what the system is. main says where its parts run and how its topic edges travel. Tests 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, not only local side effects

Hale can constrain blocking, allocation, syscalls, time, entropy, publication, spawning, and recursion across a reachable call path. What makes causality an effect rather than a separate analysis is that it obeys the same rule as the rest: a property is declared at one site and proven over everything that site can reach. Reaching, here, does not stop where the call stack does.

That is the whole of the idea. A function that publishes has not ended its influence; it has handed it to whoever subscribes, and to whoever they publish to in turn. Declaring a 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 entrypoint 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 authored once and adopted per entrypoint. Every clause is still evaluated in the adopting main's own closed world: one text, many worlds, many independent verdicts. Composition is union only, so a derived constitution can add a rule and can never replace one. Weakening isn't rejected, it's unexpressible. Binding lives in hale.toml, because which law applies is a property of where you deploy, and hale check --matrix proves every entrypoint against every environment that runs it. An entrypoint listed in no environment is an error rather than a skip, which is the one hole composition cannot close by itself.

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.

Note the shape of that last rung. A plan carries instances, routes, groups and claims, so it plays the role of a main locus one scale out: children, bus edges, and law, over separately compiled binaries. It is a composition of certified artifacts rather than a locus declaration — the plan is JSON, and there is no fleet syntax in Hale source. What recurs is the model, not the spelling. The recursion did not stop at the process boundary; it changed what a component is.

That is the whole thesis in one line, so it is worth being exact about what is claimed. Hale is not one construct wearing six costumes; it is one account of ownership, flow, closure, and law, which a value, a locus, an application, and a fleet are each a projection of. The claim is about the model, not the grammar.

Two axes, not one ladder

This page climbs one axis, and the guide climbs another, which is worth saying out loud before they read as rival accounts. Hale scales along system scale, from function scope to fleet, and along control altitude, from everyday code to explicit systems machinery. Scale asks how large the composed system is; altitude asks how much of the machinery you are choosing to control. They are independent: a single locus participates 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 ever leaving the model this page describes.

The commitments

1. Nothing stateful is ownerless. State and lifetime have a structural home.
2. No communication edge is ambient. It is named, typed, and authorized.
3. Operational behavior can be surfaced. Blocking, allocation, publication, and dependence can become contracts.
4. Failure goes somewhere structural. Recovery belongs to an owner with context.
5. Deployment is part of the program. Placement and transport are not unrelated afterthoughts.
6. At a certification boundary, unknown is not proven. A hard guarantee must fail closed. Ordinary hale check still reports some topology findings as advisories; it is hale verify, a contract, or a claim that turns not-knowing into a failure.
7. Runtime change crosses declared seams. Dynamism should move between valid arrangements, not mutate the graph arbitrarily.

The direction

Hale makes architecture declarative, then checkable, then observable, each stage handing evidence to the next rather than asking to be trusted.

shipped means implemented and specified, on v0.19 (a prerelease). It is not yet a stability guarantee: syntax, artifact schemas, and operational guarantees can still change before 1.0.

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

Otherwise: the guide, the verification surface, or the tour.