Axiom · black
Керування потоком
Знайомі if/for/while без зайвої церемонії. Різниця в тому, що loop bounds і invariants можуть стати матеріалом для proof engine.
Цикл з доведеним 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
Borrowed read-only sequence.
2
Акумулятор.
3
Loop condition гарантує i < size у тілі.
4
Тому values[i] не потребує runtime bounds check, якщо proof engine зберіг цей факт.
5
Повертаємо суму.
BREAK і CONTINUE
CONTINUE — заплановано
CONTINUE наразі ще не існує в bootstrap compiler, але входить у target surface. Документація використовує його вже зараз, щоб майбутній control-flow був послідовним.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
Перевіряємо поточний рядок.
5
CONTINUE переходить до наступної ітерації.
6
Виконується лише для непорожнього рядка.
Рекурсії немає
Пряма й непряма рекурсія заборонені. Compiler будує call graph і відхиляє цикл викликів. Для parser-ів, обходів дерев і state machines використовуйте явний stack/queue з bounded storage. Це не обмеження «бо так простіше компілятору»: воно робить worst-case stack usage аналізованим.