Practical recipes
Small programs that show why Axiom matters outside kernel development.
1. Parse HTTP Content-Length
1parse_length(text value) -> result<u32, request_error>:2 const u64 wide = text.parse_u64(value)?3 if wide > 1_048_576:4 RETURN error(payload_too_large(wide, 1_048_576))5 assert wide <= 1_048_5766 RETURN ok(u32(wide))Typed failure is part of the signature.
Parsing does not throw.
External input is checked once.
The error carries useful values.
Proof checkpoint preserves the bound.
The narrowing conversion is safe because the upper bound is known.
2. Build an HTTP response without heap allocation
1make_response(user value) -> two_pass<bytes>:2 plan:3 const usize body = json.encoded_size(value)4 const usize head = http.header_size(body)5 RETURN head + body6 build(view<u8> out):7 require out.size() >= planned_size8 const usize n = http.write_json_response(out, value)9 ensure n == planned_size10 RETURN out[0..n]Return a planned operation.
Compute exact JSON bytes.
Compute header bytes.
Total is known before writing.
Build gets storage.
Capacity proof.
One deterministic write pipeline.
Implementation proves planning and execution agree.
3. Worker tasks without a shared mutable vector
1process_batch(view<job> jobs):2 const auto parts = jobs.split_disjoint(worker_count)3 for const auto part in parts:4 spawn worker(part)5 await allCaller supplies the mutable batch.
The library returns provably disjoint views.
Spawn one task per range.
Each worker owns an exclusive range.
Structured join closes the scope.
4. Bounded DFS without recursion
1walk(tree t, view<node_id> stack):2 require stack.size() >= t.max_depth()3 usize top = 04 stack[top] = t.root()5 top = top + 16 while top > 0:7 top = top - 18 const node_id n = stack[top]9 visit(n)10 // push children with proven capacity from max_depth()Stack storage is caller-owned.
Contract replaces hope about recursive stack depth.
Explicit stack pointer.
Loop instead of recursion.
Bounds follow from top/capacity facts.
Children are pushed under a proven upper bound.