Axiom · light
Control flow
Familiar if/for/while, but loop bounds and invariants can feed the proof engine.
A loop with proven bounds
Loop boundsAxiom
1sum(view<const i32> values) -> i64:2 i64 total = 03 for usize i = 0; i < values.size(); i = i + 1:4 total = total + values[i]5 RETURN total1
Read-only borrowed sequence.
2
Accumulator.
3
The loop condition proves i < size in the body.
4
The indexed access can therefore avoid a redundant runtime bounds check.
5
Return the total.
BREAK and CONTINUE
CONTINUE is planned
CONTINUE is not yet present in the bootstrap compiler, but it is part of the target surface documented here.Target surfaceAxiom
1count_non_empty(view<const text> rows) -> usize:2 usize count = 03 for const text row in rows:4 if row.empty():5 CONTINUE6 count = count + 17 RETURN count3
Range-style loop.
4
Check the current row.
5
Continue with the next iteration.
6
Only non-empty rows reach the increment.
No recursion
Direct and indirect recursion are forbidden. The compiler checks the call graph for cycles. Tree walks and parsers use explicit bounded stacks or queues. This keeps worst-case stack usage analyzable.