examples
Programs, with their evidence.
Programs read beside what the machine says about them — run transcripts, refusals with witnesses, recorded runs replayed. Everything is captured from hale 0.19.2 at build time; the code on every page is the exact program the build verified.
Everyday Hale.
The altitude you would reach for Python or Node: arguments, files, JSON, HTTP, config — ordinary programs, each with the compiler's side of the story.
cli converter
A tool is a binary with arguments.
Read a positional argument with a default, parse it with the error addressed on the same line, print the answer. `hale build` turns it into one static executable — no interpreter, no packaging step. The break shows the fallback typing: a default that could not stand in for the parse result is refused.
Read CLI arguments & config →fn main() {
let raw = std::env::arg_or(1, "100");
let celsius = std::str::parse_int(raw) or 0;
let fahrenheit = celsius * 9 / 5 + 32;
println(raw, "°C = ", fahrenheit, "°F");
}$ hale run convert.hl
100°C = 212°FDefault with the wrong type.
- std::str::parse_int(raw) or 0
+ std::str::parse_int(raw) or "0"$ hale check convert.hl
convert.hl:3:19: type error: `or <substitute>`: fallback type `String` does not match success type `Int`
let celsius = std::str::parse_int(raw) or "0";
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^json in, json out
Parse into a type, not a tree.
The `json:` tags on the type are the whole codec: `from_json` walks the document once into a typed value, and `to_json` writes it back. A missing field is an error with a name, not a null that surfaces three calls later — and the parse is fallible, so skipping the handler is a compile error, not a runtime surprise.
Read JSON without a schema language →type Order {
id: Int `json:"id"`;
price: Int `json:"px"`;
currency: String = "USD";
}
fn main() {
let body = "{\"id\": 7, \"px\": 1899}";
let o = Order::from_json(body) or { println("bad order: ", err.field); return; };
let marked = Order { id: o.id, price: o.price * 105 / 100, currency: o.currency };
println(Order::to_json(marked));
}$ hale run orders.hl
{"id":7,"px":1993,"currency":"USD"}Skip the error the parse can raise.
- Order::from_json(body) or { println("bad order: ", err.field); return; }
$ hale check orders.hl
orders.hl:9:13: type error: error not addressed: this expression's fallible result must be handled with an `or` clause (`or raise`, `or <fallback>`, `or handler(err)`) or a `match`
let o = Order::from_json(body);
^^^^^^^^^^^^^^^^^^^^^^files & directories
Walk a directory, count what matters.
Write, list, read, and summarize — the one-shot `std::io::fs` calls, each fallible and each addressed where it happens. Inside a `fallible` helper an unhandled error propagates to the caller; at `main` the buck stops, and the break shows the compiler refusing to let it ride.
Read files & the filesystem →@form(vec)
locus Names { capacity { heap items of String; } }
@form(vec)
locus Lines { capacity { heap items of String; } }
fn count_errors(text: String) -> Int {
let lines = Lines { };
std::str::split_into(text, "\n", lines);
let mut errors = 0;
for line in lines.items {
if std::str::starts_with(line, "ERROR") { errors += 1; }
}
return errors;
}
fn summarize() fallible(IoError) {
std::io::fs::mkdir("logs") or discard;
std::io::fs::write_file("logs/api.log", "ok\nERROR timeout\nok\n") or raise;
std::io::fs::write_file("logs/db.log", "ERROR lock\nERROR retry\n") or raise;
let found = Names { };
let count = std::io::fs::list_dir_count("logs") or raise;
let mut i = 0;
while i < count {
found.push(std::io::fs::list_dir_at("logs", i) or raise);
i += 1;
}
let names = Names { };
found.sort_into(names);
for name in names.items {
let text = std::io::fs::read_file("logs/" + name) or "";
println(name, ": ", count_errors(text), " error(s)");
}
}
fn main() {
summarize() or { println("io error"); };
}$ hale run logsum.hl
api.log: 1 error(s)
db.log: 2 error(s)Let the helper's errors ride past main.
- summarize() or { println("io error"); };
+ summarize();$ hale check logsum.hl
logsum.hl:38:5: type error: error not addressed: this expression's fallible result must be handled with an `or` clause (`or raise`, `or <fallback>`, `or handler(err)`) or a `match`
summarize();
^^^^^^^^^^^http client
One call, one response, errors in the type.
`std::http::get` returns a response or an error with a kind — connection refused and a bad URL are different values, not different string prefixes — and the or-block is where the caller decides what a failure means. Run output is not captured at build time because CI has no network.
Read HTTP clients & servers →fn main() {
let url = std::env::arg_or(1, "https://hale-lang.org/llms.txt");
let resp = std::http::get(url) or {
println("fetch failed: ", err.kind);
return;
};
let body = std::str::from_bytes(resp.body);
println("status ", resp.status, ", ", len(body), " bytes");
}layered config
Argument beats environment beats default.
One resolver states the precedence — positional argument, then `$APP_HOST`, then the built-in — and an app locus receives the result as typed params. Params are a contract, not a bag: constructing one that the locus never declared is the break, and the diagnostic names the field.
Read CLI arguments & config →locus App {
params { host: String = "0.0.0.0"; port: Int = 8080; }
run() {
println("listening on ", self.host, ":", self.port);
}
}
fn main() {
let cfg = std::cli::Resolver {
env_prefix: "APP_",
argv_keys: "host\nport\n",
};
App {
host: cfg.get("host", "0.0.0.0"),
port: cfg.get_int("port", 8080),
};
}$ hale run configured.hl
listening on 0.0.0.0:8080Configure a param that doesn't exist.
- host: cfg.get("host", "0.0.0.0"),
+ hostname: cfg.get("host", "0.0.0.0"),$ hale check configured.hl
configured.hl:15:9: type error: locus `App` has no field `hostname`
hostname: cfg.get("host", "0.0.0.0"),
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^webassembly
The same locus, compiled for the browser.
`target wasm { }` is a declaration the typechecker enforces: the portable stdlib and the typed bus work as they do natively, and the syscall-backed namespaces are refused at compile time — the break reaches for `std::http` inside the sandbox and is told exactly why not. `@export` methods become the module's exports; the page drives them.
Read WebAssembly & the browser →Run Hale in the playground ↗target wasm { }
@ffi("js") fn console_log(msg: String);
@export locus Counter {
params { clicks: Int = 0; }
birth() { console_log("counter ready"); }
fn bump() {
self.clicks += 1;
console_log("clicks: " + to_string(self.clicks));
}
}Reach for sockets inside the sandbox.
- birth() { console_log("counter ready"); }
+ console_log("counter ready");
+ let r = std::http::get("https://example.com/config") or { return; };
+ }$ hale check counter.hl
counter.hl:10:17: type error: `std::http::get` is unavailable under `target wasm`: the `std::http` server is built on raw TCP and isn't available in the browser
let r = std::http::get("https://example.com/config") or { return; };
^^^^^^^^^^^^^^Complete systems, with their evidence.
Full systems read top to bottom: keyed fan-out, causal boundaries, certified hot paths, fleet composition — the code on every page concatenates to the exact program the build verified.
80 lines · chat.hl
A chat server that runs itself
Rooms as keyed topics, a sealed session signer, supervision that recovers on the page, and a law about who may sign.
Read the whole system →23 lines · intake.hl
Two binaries, one law
Separate builds sharing a topic over a socket, composed and checked as a fleet — drift in either binary fails the plan.
Read the whole system →81 lines · pipeline.hl
A sharded sensor pipeline
Keyed fan-out, placement, a certified hot path, a causal boundary — and the whole run recorded and replayed.
Read the whole system →One guarantee at a time.
The same discipline at snippet scale: the honest version and a one-line break, with the compiler's actual refusal beside it.
sharded job queue
Let the topic own the routing table.
A keyed topic delivers each job only to the worker whose key it carries — the handler never sees the other shards. And the routing contract is typed: the break shows what happens when the payload stops carrying the field the topic shards on.
Read the job-queue tutorial →type Job { queue_id: Int; body: String; }
topic JobReady { payload: Job; keyed_by queue_id; }
locus Worker {
params { queue_id: Int = 0; done: Int = 0; }
bus { subscribe JobReady as perform where key == self.queue_id; }
fn perform(job: Job) {
self.done = self.done + 1;
println("worker ", self.queue_id, " took ", job.body);
}
}
main locus App {
params { a: Worker = Worker { queue_id: 1 }; b: Worker = Worker { queue_id: 2 }; }
bus { publish JobReady; }
run() {
JobReady <- Job { queue_id: 1, body: "resize" };
JobReady <- Job { queue_id: 2, body: "transcode" };
JobReady <- Job { queue_id: 1, body: "thumbnail" };
}
}
fn main() { App { }; }$ hale run workers.hl
worker 1 took resize
worker 2 took transcode
worker 1 took thumbnailDrop the field the topic shards on.
- type Job { queue_id: Int; body: String; }
+ type Job { body: String; }$ hale check workers.hl
workers.hl:2:41: type error: topic `JobReady`'s `keyed_by` references field `queue_id`, which does not exist on payload type `Job`
topic JobReady { payload: Job; keyed_by queue_id; }
^^^^^^^^
workers.hl:17:27: type error: type `Job` has no field `queue_id`
JobReady <- Job { queue_id: 1, body: "resize" };
^^^^^^^^^^^
workers.hl:18:27: type error: type `Job` has no field `queue_id`
JobReady <- Job { queue_id: 2, body: "transcode" };
^^^^^^^^^^^
workers.hl:19:27: type error: type `Job` has no field `queue_id`
JobReady <- Job { queue_id: 1, body: "thumbnail" };
^^^^^^^^^^^causal boundary
State what may influence a subsystem.
The dependency set is checked transitively through the bus graph — a republisher cannot launder an undeclared source into this locus. Subscribe to one topic the declaration does not name, and the build stops.
Read effects and causality →type Snapshot { id: Int; }
type Config { limit: Int; }
type Tick { n: Int; }
topic RiskSnapshot { payload: Snapshot; }
topic RiskConfig { payload: Config; }
topic Clock { payload: Tick; }
@effects(depends: {RiskSnapshot, RiskConfig})
locus RiskView {
params { seen: Int = 0; }
bus {
subscribe RiskSnapshot as update;
subscribe RiskConfig as configure;
}
fn update(s: Snapshot) { self.seen = self.seen + 1; }
fn configure(c: Config) { self.seen = self.seen + 1; }
}
main locus App {
params { v: RiskView = RiskView { }; }
bus { publish RiskSnapshot; publish RiskConfig; publish Clock; }
run() { RiskSnapshot <- Snapshot { id: 1 }; }
}
fn main() { App { }; }Listen to the clock without declaring it.
- subscribe RiskConfig as configure;
+ subscribe Clock as tick;$ hale check risk-view.hl
risk-view.hl:9:10: type error: declared dependency set violated: `RiskView` can transitively depend on `Clock` through the bus, which its `@effects(depends: …)` does not declare. It is subscribed directly by `RiskView`. Add the subject to the set, or route the input through a subject this locus doesn't reach.
@effects(depends: {RiskSnapshot, RiskConfig})
^^^^^^^certified hot path
Make the performance assumption reviewable.
This path does not merely intend to avoid the kernel, waiting, and allocation — the compiler follows its callees and rejects the build when the promise stops being true, counting the exact allocation that broke it.
Read effects and contracts →type Sample { a: Float; b: Float; w: Float; }
@no_block @no_syscall @deterministic
@budget(alloc_per_call = 0)
fn score(sample: Sample) -> Float {
return sample.a * sample.w + sample.b * (1.0 - sample.w);
}
fn main() {
let s = Sample { a: 0.9, b: 0.4, w: 0.75 };
println("score ", score(s));
}$ hale run score.hl
score 0.775Build a label on the hot path.
- return sample.a * sample.w + sample.b * (1.0 - sample.w);
+ let label = "sample-" + to_string(sample.w);$ hale check score.hl
score.hl:5:4: type error: hot-path budget exceeded: `score` declares `@budget(alloc_per_call = 0)` but the compiler counts 1 arena allocation(s) per call. For a zero-alloc hot path: hoist per-iteration allocations to reused fields, read with `recv_into` into a reused `std::bytes::BytesBuilder`, and keep locus instantiation out of the fn. If the allocation is intentional, drop `@budget` for `@unbounded fn`.
fn score(sample: Sample) -> Float {
^^^^^
score.hl:6:17: type error: counts against `score`'s alloc budget: a string concatenation (each `+` builds a fresh String)
let label = "sample-" + to_string(sample.w);
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^confined secret
State what the rest of the program cannot reach.
A sealed locus owns its params outright: everyone else holds a phone number, not the key. Reading the field from outside is not a convention violation — it fails the build, and the diagnostic names the method to call instead.
Read the secrets article →@sealed locus Signer {
params { key: Int = 7; }
@effects(is: {secret_use})
fn sign(msg: Int) -> Int { return msg * 31 + self.key; }
}
locus Gateway {
params { s: Signer = Signer { }; }
fn tag(msg: Int) -> Int {
return self.s.sign(msg);
}
}
fn main() {
let g = Gateway { };
println("sig ", g.tag(41));
}$ hale run signer.hl
sig 1278Read the key instead of asking for a signature.
- return self.s.sign(msg);
+ let direct = self.s.key;
+ return msg * 31 + direct;$ hale check signer.hl
signer.hl:10:22: type error: `Signer` is `@sealed`: its `params` are readable only from inside its own methods, and `Signer.key` reads one from outside — call one of its methods instead (sign)
let direct = self.s.key;
^^^^^^^^^^law with a witness
Write the rule; get the counterexample.
The claim is two lines of law about the program itself. Wire a signer into the plugin host and the violation names the exact call chain that crosses the boundary — a counterexample, not a lint.
Read the claims article →@sealed locus Signer {
params { key: Int = 7; }
@effects(is: {secret_use})
fn sign(msg: Int) -> Int { return msg * 31 + self.key; }
}
locus Gateway {
params { s: Signer = Signer { }; }
fn issue(msg: Int) -> Int { return self.s.sign(msg); }
}
locus PluginHost {
params { n: Int = 0; }
fn render(x: Int) -> Int { return x + self.n; }
}
group plugins = { PluginHost };
main locus App {
params { g: Gateway = Gateway { }; p: PluginHost = PluginHost { }; }
claims {
plugins_never_sign:
forbid reaches(plugins, effects(secret_use));
}
run() { let sig = self.g.issue(41); }
}
fn main() { App { }; }Hand the plugin host a signer.
- locus PluginHost {
- params { n: Int = 0; }
- fn render(x: Int) -> Int { return x + self.n; }
- }
+ params { n: Int = 0; s: Signer = Signer { }; }
+ fn render(x: Int) -> Int { return self.s.sign(x); }$ hale check app.hl
app.hl:22:9: type error: claim `plugins_never_sign` violated: `plugins` reaches `effects(secret_use)` — witness: `PluginHost::render` -> `Signer::sign`
plugins_never_sign:
^^^^^^^^^^^^^^^^^^
app.hl:14:39: type error: claim `plugins_never_sign`: the boundary into `effects(secret_use)` is crossed by this call
fn render(x: Int) -> Int { return self.s.sign(x); }
^^^^^^^^^^^^^^
app.hl:1:15: type error: claim `plugins_never_sign`: the forbidden destination `Signer` is declared here
@sealed locus Signer {
^^^^^^record & replay
The run becomes a file you can run again.
Twenty readings of a random sensor, recorded — schedule and journaled inputs both. The replay serves the same random values back in the same per-consumer order and the comparison signs off. No logging calls, no instrumentation: the runtime is the thing delivering the messages.
Read the record & replay article →type Reading { v: Int; }
locus Aggregator {
params { total: Int = 0; count: Int = 0; }
bus { subscribe Sensor as ingest; }
fn ingest(r: Reading) {
self.total = self.total + r.v;
self.count = self.count + 1;
}
}
topic Sensor { payload: Reading; }
locus Probe {
bus { publish Sensor; }
run() {
let mut i = 0;
while i < 20 {
Sensor <- Reading { v: std::rand::next_int(100) };
i = i + 1;
}
}
}
main locus App {
params { a: Aggregator = Aggregator { }; p: Probe = Probe { }; }
placement { p: pinned(core = 0); }
run() { std::time::sleep(700ms); }
}
fn main() { App { }; }$ LOTUS_OBS_RECORD=session.halerec hale run sensor.hl
$ hale replay session.halerec sensor.hl --allow-live-effects --diff
hale replay: journal served fully — 0 divergences, 20 consumes
replay matches the recording: 20 consumes across 1 consumers; canonical payloads identical, raw ABI payload sizes matched (110 ring records, 20 journal reads)Try the full progression.
The browser tour moves from ordinary functions to loci, typed topics, supervision, and deployment without changing tools.
Open the playground