Effects in Hale<br>/articles Article 31 July 2026 v0.12.0<br>Effects in Hale<br>Most concurrent systems languages give you tools to write correct code and then ask you to keep it that way. Hale takes a different stance on a narrow but high-leverage slice of that problem: a function can declare what it is allowed to reach, and the compiler proves the claim over the entire call graph.

The mechanism is deliberately lightweight. Annotations are opt-in. Once present, the proof is total and incompleteness fails closed. The vocabulary is systems-oriented rather than academic. The same surface also supports quantitative budgets, per-lifecycle-phase contracts, and causal tracking across the typed message bus.

Why effects at all

In a long-running concurrent process the properties that actually matter on the hot path are usually negative:

this handler allocates nothing

this function never blocks

this computation is a pure function of its inputs (no clock, no entropy, no environment)

this publish cannot transitively cause filesystem I/O

after startup, the steady-state phase performs no dynamic allocation

These are the properties that keep RSS flat, latency predictable, and behavior replayable. Hale’s effect system exists to make them checkable at compile time instead of discoverable under load.

Effect classes

The checker works with a fixed set of classes:

ClassMeaningTypical sourcesyscallKernel entry: filesystem, sockets, processes, terminal, stdioread_file, printlnblockWaits that hold a thread or worker turnsleep, blocking recv, HTTP clienttimeReading a clockmonotonic_nsentropyReading randomnessnext_intenvReading environment or argvenv::varffiCrossing into an @ffi declarationany foreign functionpublishSending on the busOrders spawnInstantiating a locusWorker { }recursionCycle in the call graphself-recursive functionallocArena allocation (primarily for phase contracts)constructing a buffer<br>Two distinctions matter in practice.

First, println is a syscall. Writing to a stream is write(2); it can block. A certificate that permitted debug printing would not be certifying what it claimed.

Second, reading an effect source is different from operating on a supplied value. std::time::time_from_unix(n) is pure; std::time::monotonic_ns() is not. The same split applies to parsing versus fetching, and to formatting versus sampling entropy. This is what makes @deterministic useful rather than merely restrictive: a function that never reads a clock, randomness, or the environment is a function of its inputs, so replaying the inputs replays the behavior.

The standard library publishes every function’s classes alongside its signature (hale doc --stdlib). The catalogue and the checker share the same registry, so they cannot disagree.

Declaring what a function may reach

The general form is:

@effects(none: {syscall, block})

fn decode(b: Bytes) -> Msg { ... }

@effects(none: {time})

fn backoff(n: Int) -> Int { ... }

@effects(publish: {OrderFill})

fn route(o: Order) { ... }

Msg { ... }@effects(none: {time})fn backoff(n: Int) -> Int { ... }@effects(publish: {OrderFill})fn route(o: Order) { ... }">

none: {…} forbids the listed classes. publish: {…} states exactly which topics the function may send on; Hale’s topic set is closed, so the check is precise.

Common contracts have short names that expand to the same thing:

ShorthandExpands to@no_syscall@effects(none: {syscall})@no_block@effects(none: {block})@no_ffi@effects(none: {ffi})@no_publish@effects(none: {publish})@no_spawn@effects(none: {spawn})@no_recursion@effects(none: {recursion})@deterministic@effects(none: {time, entropy, env})<br>They compose. A typical hot-path certificate is one line:

@no_block @no_syscall @deterministic @no_recursion @hot

@budget(alloc_per_call = 0)

fn on_tick(a: Int, b: Int) -> Int { ... }

Int { ... }">

When an assertion fails, the diagnostic names the path, not merely the verdict:

effect assertion violated: `on_tick` must not reach `block`,

but reaches on_tick -> helper -> nap [std::time::sleep — a blocking operation …].

helper -> nap [std::time::sleep — a blocking operation …].">

The checker follows ordinary calls, self methods, and calls made through handles. Moving an effect behind a locus the function still calls does not hide it. The workable patterns are to pass the already-computed value in, or to publish to a locus the asserting function does not reach.

Incompleteness fails closed. A standard-library call the registry cannot classify is treated as “may do anything.” An assertion is a claim about everything reachable; anything unknown is exactly what it must not certify.

Quantitative budgets

@budget counts concrete resources:

@budget(alloc_per_call = 0, stack_bytes = 4096, block_points = 0)

fn on_frame(x: Int) -> Int { ... }

@budget(publish = 1)

fn reply(o: Order) { ... } // exactly-once reply

@budget(fanout = 8)

fn notify(e: Ev) { ... } // bounded amplification

Int { ... }@budget(publish = 1)fn reply(o: Order) {...