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.

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");
    }
}

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. It can also state which subjects may transitively influence a locus, following the path through republishers on the bus graph.

@effects(depends: {Reading, ConfigChanged})
locus Rollup {
    bus {
        subscribe Reading as add;
        subscribe ConfigChanged as configure;
    }
}

The Hale constitution

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. Unknown is not proven. A hard guarantee must fail closed.
7. Runtime change crosses declared seams. Dynamism should move between valid arrangements, not mutate the graph arbitrarily.

The direction

Hale first makes architecture declarative, then checkable, then observable. The next steps are deterministic replay and verified deployment adaptation. They are marked as RFC work, not shipped features.

Continue with the guide, inspect the verification surface, or run the tour.