Практичні приклади
Кілька невеликих програм, які показують, навіщо Axiom потрібен не лише kernel-розробнику.
1. Парсимо 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))Return type документує failure cases.
Парсер не кидає exception.
Runtime input перевіряється один раз.
Ми зберігаємо корисні дані в error.
Proof checkpoint показує analyzer-у/читачу bounded fact.
Narrowing до u32 безпечний, бо верхня межа вже доведена.
2. Формуємо response без heap
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]API повертає planned operation.
Рахуємо exact JSON bytes.
Рахуємо HTTP header.
Знаємо total до запису.
Build отримує storage.
Capacity proof.
Один deterministic write pipeline.
Implementation доводить, що план і фактичний output узгоджуються.
3. Worker tasks без 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 передає mutable batch.
Library повертає views, для яких compiler має proof disjointness.
Створюємо task на кожну частину.
Кожен worker отримує exclusive range.
Structured join завершує scope.
4. Bounded DFS без рекурсії
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 приходить від caller-а.
Передумова замінює «сподіваємося, recursion stack не скінчиться».
Явний stack pointer.
Цикл замість recursive call.
Bounds випливають із top і capacity contract.
Children додаються з перевіреним upper bound.