Hale.

The bet.

Hale’s position is that the distance between how you describe a system out loud and what you type should be near zero — and that the same property that helps a human helps a model. One primitive, the locus, stands in for class, module, package, actor, and service. Loci communicate over a typed topic bus and never reach sideways into each other; a main locus declares placement (threads, cores, NUMA nodes) and bindings (in-process queue, Unix socket, shared-memory ring), so deployment shape is an edit to one block, not a rewrite.

LLM authorship is one of four stated design pillars, not the whole thesis, and the argument for it is subtractive rather than additive: there is no async colouring, no lifetime annotation, no lock vocabulary, no iterator/closure machinery. The constructs a model is most likely to hallucinate are absent, so a large class of plausible-looking wrong programs does not parse.

The verification story is what earns the camp placement. Per-function effect certificates (@no_syscall, @deterministic, @budget, @effects(only: …)) are proven transitively through helpers and imported libraries. Above them sit claims: named sentences over the assembled program graph — forbid reaches(A, B), only edges A -> B { publish T; }, count publishers(topic T) <= 1, allocation bounds on paths — declared in the main locus, evaluated by hale check as errors, lowered to zero runtime code. Where the graph cannot be resolved, the checker refuses rather than guesses.

Unknown means violation.

What it looks like.

topic Metrics { payload: Metric; }
locus DeltaTriage {
bus { subscribe Tasks as on_task; publish Metrics; }
fn on_task(t: Task) {
Metrics <- Metric { n: t.id };
}
}
group delta_wing = { DeltaTriage };
group gamma_wing = { GammaResearch };
main locus Org {
claims {
iso_dg: forbid reaches(delta_wing, gamma_wing);
}
}

This program fails to check, and the diagnostic returns the route:

claim `iso_dg` violated: `delta_wing` reaches `gamma_wing` —
witness: `DeltaTriage::on_task` -(publishes "Metrics")-> `GammaResearch::on_metric`

The witness is a minimal countermodel in the program’s own vocabulary, with secondary diagnostics at the publish site, the subscription, and the destination — the compiler tells you where to edit, not just that you are wrong.

The agent tooling ships in the compiler binary itself: hale mcp exposes the checker, build, tests, the bus graph, placement, and spec search as MCP tools, and the checked-in AGENTS.md is treated as load-bearing surface rather than documentation garnish. The topology the claims are checked against can be dumped as a versioned JSON artifact and re-checked in CI, so an agent (or a reviewer) can diff the architecture, not just the text.

Certain workloads are still outperformed by mainstream languages; the cross-language comparison grid, run by the project on a single machine, is tracked in hale-lang/bench with the losses stated alongside the wins.