Почніть звідси
Axiom для програмістів, які вже вміють писати програми, але не хочуть ставати експертами з UB, ABI та формальних доказів, щоб отримати передбачувану систему.
Axiom — строго типізована системна мова, де компілятор намагається довести коректність операції до запуску. Її ідея не в тому, щоб ускладнити програмування доказами, а в тому, щоб зробити небезпечні стани незручними або взагалі невиразними.
CONTINUE і частина stdlib тут документуються як запланований стандарт.Для веб-розробника
Думайте про Axiom як про мову, де TypeScript-подібна вимога «не дай мені зробити дурницю» поширена аж до пам’яті, потоків і hardware.
Для системного коду
Немає exceptions, raw pointers у звичайній мові, прихованого heap і недоведеного shared mutable state.
Для embedded
Compiler може знати upper bounds пам’яті, lifetime scratch-буферів і capability цільового CPU.
Перша програма
Почнемо не з «Hello, world», а з маленької функції, де вже видно стиль Axiom.
1discounted_total(i64 price, i64 percent) -> i64:2 require price >= 03 require percent >= 04 require percent <= 1005 RETURN price - (price * percent / 100)67main -> i64:8 RETURN discounted_total(1250, 20)Оголошуємо функцію. Типи параметрів і return type завжди явні.
require — обов’язок caller-а. Виклик допустимий лише якщо компілятор може довести, що ціна не від’ємна.
Те саме для нижньої межі знижки.
І для верхньої. Це не «документація для людини», а умова для аналізатора.
Звичайний арифметичний вираз. Доведені умови можуть дозволити прибрати зайві runtime checks.
main без параметрів. Немає окремого function keyword.
Константи відомі компілятору, тому всі три require тут тривіально доводяться.
Що Axiom навмисно не робить
Axiom не ставить за мету бути C++ з іншим синтаксисом. Немає exceptions, RTTI, raw pointer API як звичайного інструмента, неявних race condition, рекурсії чи «сподіваємося, що buffer достатній». Якщо небезпека неминуча на hardware/ABI boundary, вона має бути короткою, видимою і позначеною як sus.
Як читати цю документацію
Спочатку пройдіть «Модель мислення» → «Контракти» → «View» → «Детермінована пам’ять». Після цього синтаксис Axiom почне виглядати логічно. Розділи про compiler, target і hardware вже пояснюють, як ця семантика доходить до ELF, ABI й драйверів.