Language features

Unless a line says otherwise, everything here is implemented, statically checked, and specified: the syntax parses, the checks run, and the runtime path exists. For exact semantics, read the specification. It describes current behavior, and this page follows it.

Not every entry carries the same kind of evidence, so the ones that differ are marked: Linux a platform-specific path, modeled checked as a formal model whose correspondence to the shipped code is maintained by hand, andreserved named and specified but not yet built.

One primitive

• The locus, one construct where other languages have class, module, package, actor, and service. An app, a cache, a handler, and a library are all loci; composition is locus-in-locus.
• Lifecycle: birth / run /dissolve, params with defaults, parent–child nesting with deterministic cleanup on dissolve.
• Perspectives: live hot code-swap at pointer-flip cost: reperspective carries state across and re-points bus edges without dropping messages.
• Modes: bulk / harmonic /resolution projections over capacity slots, for programs that reshape under load.

The typed bus

• Topics as declarations: topic T { payload: P; } with wire subjects, routing keys (keyed_by), and per-topic bounds with an explicit backpressure contract (or wait).
• Traffic is declared, not reached for: peer loci do not reference one another, they communicate through a declared topic, and messages are copies. Subscription and publish are declared surface, so the compiler sees the whole message graph.
• Topology checked at compile time: hale check rejects payload mismatches and unconditional intra-locus re-entry. It reports orphaned topics, cross-locus cycles, and statically unbounded backpressure as advisories.hale verify promotes every advisory into a failing discipline gate, so a project chooses its own strictness without the language pretending the two kinds of finding are one.

Types & data

• Structural interfaces, an interface is satisfied by shape; there is no impl I for L ceremony.
• Synthesized forms, @form(vec | hashmap | ring_buffer | lru_cache) generates type-specialized collections; bounded[T; N] for fixed capacity. No generics ceremony on the everyday path.
• Element chains: xs.filter(it > 2).count() compiles to one loop, allocation-free, with no closure or iterator object.
• Money and time as types, Decimal, typed timestamps and durations; inference for let, returns, and locus params; f-strings.

Failure

• fallible(E) in the type, every fallible call is addressed at the call site with a disposition (or default, or raise, or wait, …). No exceptions, no panic.
• Failures travel vertically: a child's failure goes to its parent, which owns recovery. There is no sideways error channel to leak through.
• closure assertions: declared invariants audited by the runtime at phase boundaries.

Law: effects, claims, constitutions, fleets

• Effect certificates, ten effect classes (syscall, block, time, entropy, alloc, …); opt-in assertions (@no_block, @deterministic, @effects(only: …)) proven transitively over the whole call graph, with quantitative budgets (@budget) and per-lifecycle-phase contracts (@phase_effects). Incompleteness fails closed.
• Claims, named sentences over the assembled program graph, declared in main, checked as errors, zero runtime cost: forbid reaches, only edges, require / cover / count, bound, interposition (avoiding), lifecycle slices (during). Violations return a minimal countermodel in your own spelling.
• Constitutions, one claimset adopted by many entrypoints, composed by union only (weakening is unexpressible), bound per deployment target in hale.toml and proven pairwise by hale check --matrix.
• Fleets, per-application topology artifacts compose into a deployment model; cross-binary claims with cross-binary witnesses. Only an explicit route creates an edge. Signing and binary attestation carry the certificate to the machine that deploys it.
• The topology artifact: byte-reproducible JSON with source maps, an integrity digest, and every claim verdict; commit it and diff the architecture in review, not just the text.

Memory & runtime

• Arena-per-locus: no garbage collector, no borrow checker, no lifetime annotations; memory frees deterministically when a locus dissolves.
• Model-checked synchronizationmodeled: hand-transcribed models of the runtime's concurrent protocols (lock-free bus, mailboxes, rings, arenas) are explored with GenMC in substrate CI. The models check the synchronization logic across permitted interleavings; their correspondence with the production runtime is maintained by hand and remains part of the trusted base. What that does and does not establish →
• Static dispatch by default, devirtualized bus delivery and calls; cooperative pools with epoll-backed parking; pinned threads and replicas = K fan-out declared in main. NUMA-aware arena placement and cache-domain pinningLinux.

Deployment

• Same source, many shapes, placement and bindings in main decide threads, cores, and transports. A test, one binary, or a mesh of binaries is an edit to one block.
• Transports: in-process queues, Unix sockets, zero-copy shared-memory rings, and broker adapters written as ordinary loci; pluggable codecs.

Interop

• C FFI: @ffi("c") bindings with [ffi] csrc compilation, both directions across the boundary.
• WebAssembly: wasm32 target with @export loci and @ffi("js"); the playground runs the result client-side.
• Packages: hale fetch vendors pinned git dependencies; pond is the contributed library collection.

Standard library

• Path-called, no imports: processes, env, filesystem, TCP/UDP (zero-copy readers), TLS, HTTP (router and client), JSON (including a streaming builder), metrics, logging with sinks, compression, tar, crypto and hashing, encodings, randomness, strings, regex, sets, time.hale doc --stdlib publishes each function's effect classes from the same registry the checker proves against.

Toolchain

• Everything ships in the one hale binary — build, run, check, verify, test, bench, fmt, doc, fetch, fleet — with the language server and the MCP server compiled into it, so an editor, a CI job and a coding assistant all read the same diagnostic.The toolchain, in full →

Platforms

Three different questions, easy to conflate: where a prebuilt compiler exists, where one can be built, and what a build can emit.

• Prebuilt compiler: Linux x86-64, Linux ARM64, and macOS on Apple Silicon, on GitHub Releases and selected automatically by the install script.
• Builds from source: the above, plus Intel macOS. Needs LLVM 18 dev libraries and clang.
• Emits: native binaries for Linux and macOS, and wasm32 objects for the browser.x86_64-pc-windows-msvc is named by hale --list-targets and refused with a precise error rather than a link failure reserved.

The frontier

Reserved surface, awaiting a workload that earns it: async/await keywords, traits with explicit impls, macros, richer form shapes. The runtime frontier is cost, a cheaper call protocol and spawn path. The spec stays the arbiter: it describes what ships, and this page follows it.

Want to nudge a priority? The fastest signal is a real program that needs it, see community.