Typed broker and deployment bindings
In-process dispatch, Unix, UDP, shared-memory paths, codecs, and user adapter loci.
proof
What is checked, what is measured, and what is still open.
Hale makes broad architectural claims. This page keeps them tied to compiler rules, runtime evidence, and public limitations. Ambition is useful only when the status is legible.
Effects, budgets, causes, and depends
Operational and causal contracts with witness paths.
Structural lifetime and supervision
Owned regions, child lifecycle, failure propagation, and restart policy.
Observation plane
Runtime birth, dissolve, publish, delivery, and transport evidence.
Bundle-level claims and the topology artifact
Named sentences over the assembled graph — isolation, grants, coverage, cardinality, interposition, bounds — with countermodel witnesses and a committed model baseline.
Deterministic record and replay
A self-describing execution record built from effects, deployment, and observation.
Deployment elaboration and meta-scheduling
Candidate arrangements verified before activation or transition.
Typed bus topology
Topic declarations establish payload type and publish/subscribe authority. The compiler inspects the closed-world graph for orphaned subjects, impossible handlers, routing-policy errors, and re-entrant cycles.
Bus semantics →Effect reachability
Assertions such as @no_syscall,
@no_block, @deterministic, and
@budget are checked across reachable calls, imported
seeds, handles, and interface dispatch.
Causal bus contracts
causes: follows outward influence across publishes.
depends: walks backward through subscriptions and
republishers to check the complete set that may reach a locus
over the bus graph — including through a republisher in
another library. Influence that travels outside the bus is not
part of that closure.
System claims
Groups name the domains; the main locus states the law:
forbid reaches, only edges grants,
require/cover/count,
interposition via avoiding, and capability bounds.
Violations are errors with countermodels, and the checked model
exports as a diffable artifact under a shape hash.
Structural lifetime
Loci own regions and children. The compiler enforces managed-entity rules; the runtime dissolves the owned structure deterministically and reports residency when growth needs inspection.
Memory and lifetime →Supervised failure
Lifecycle failures travel to an owning parent. Binding startup failures refuse birth instead of installing a route that silently accepts and drops messages.
Failure and supervision →Concurrent substrate
Low-level runtime primitives are model-checked under legal thread interleavings in CI. This narrows the trusted base beneath queues, mailboxes, maps, and arenas.
Inspect the repository →operational witness
The diagnostic names the call path.
A hard rule is useful only when a rejection shows how the forbidden behavior became reachable.
hale check
effect assertion violated:
price must not reach syscall
reachable path:
price
-> Book.price_for
-> Book.reload
-> std::io::fs::read_file hale check
declared dependency set violated:
StatedCarry can transitively depend on SumLookup
Path:
subject SumLookup
-> Launderer
-> subject Recalled
-> StatedCarryarchitectural witness
The path continues through the broker.
Local inspection cannot see a dependency hidden behind a republisher. The bus graph can, and the witness should name every step.
system witness
The law names its countermodel.
A bundle-level claim quantifies over every represented path. When the assembled graph escapes its declared law, the diagnostic returns the route — calls and message hops — that makes the sentence false.
hale check
claim `iso_dg` violated:
`delta_wing` reaches `gamma_wing`
witness:
delta::Triage::on_task
-(publishes "org.metrics")->
gamma::Research::on_metricreproduce it
The checks ship with the language.
The command line, editor integration, CI, and MCP server all use the compiler's structured diagnostics. The quickest evaluation is to run the examples and make the compiler disagree with you.
toolchain
hale check .
hale check . --dump-topology
hale test .
hale verify .
hale bench .
hale doc --stdlib
hale lsp
hale mcpthe boundary
The proof boundary is public too.
The checks are sound, not complete
Every analysis here is a conservative over-approximation. When the compiler cannot resolve something it treats it as may-do-anything and the contract fails, rather than assuming the best and passing. That is the correct direction, and it means a rejected program is sometimes a limit of the analysis rather than a defect in the code.
Closed-world reasoning has an edge
The guarantees derive from a closed call graph, a closed topic
set, and a classified standard library. Influence that leaves
that world — through @ffi, through a transport to
another binary, through the operating system — is outside what
the compiler can follow, and the contracts say so rather than
pretending otherwise.
Cost models are estimates, behaviour is not
Effect classes, publish sets, and causal sets are checked facts. The quantitative budgets are measured against what the compiler can see at the source level, before the backend has finished deciding layout and inlining, so treat those numbers as bounds on the program you wrote rather than on the instructions that ultimately run.
Specific open questions live in the issue tracker, where they can be argued with and closed. A storefront is the wrong place to keep a list that has to be correct on a particular Tuesday.
What this page does not claim
Hale does not prove arbitrary application correctness, make lossy transports reliable, or remove the need to choose sensible bounds and recovery policy. It makes more of those choices visible, checkable, and attributable to the architecture that owns them.