Модель мислення Axiom
Головна зміна не синтаксична: у Axiom ви пишете не лише «що зробити», а й які умови роблять операцію допустимою.
У типовому коді ми часто покладаємося на неявні припущення: індекс правильний, buffer досить великий, task уже завершився, pointer ще живий. Axiom перетворює такі припущення на речі, які compiler має бачити.
Правило одного речення
Тобто операція або вже має доказ безпеки, або створює конкретну умову, яку хтось мусить довести.
Приклад: API без «може впасти»
1first_byte(view<const u8> data) -> u8:2 require data.size() > 03 RETURN data[0]45main -> u8:6 const u8 packet[] = { 0x41, 0x58 }7 view<const u8> bytes = packet8 RETURN first_byte(bytes)Функція приймає borrowed view, а не raw pointer + length.
Ми явно формулюємо передумову: порожній view сюди передавати не можна.
Індекс 0 безпечний, бо передумова це вже довела.
Масив має lifetime всього main.
view не володіє масивом. Compiler пов’язує його lifetime з packet.
Compiler бачить, що розмір packet дорівнює 2, отже виклик законний.
Чим це відрізняється від assert
require не означає «перевірити в runtime і аварійно завершитися». Це proof obligation. Якщо compiler не може довести умову — збірка завершується помилкою. Якщо ви спеціально хочете runtime-перевірку, для цього є runtime_assert.
Детермінованість — не тільки однаковий output
У Axiom детермінованість включає передбачувану пам’ять, зрозумілі lifetime, явні effect-и паралельних задач, стабільний lowering і відсутність прихованої алокації. «Програма працює» — слабша вимога, ніж «ми знаємо, скільки ресурсів їй потрібно і чому вона не зайде в недопустимий стан».
Що таке sus
sus — внутрішня й діагностична назва для конструкції, яку compiler не може нормально довести або яка переходить trusted boundary. Наприклад, MMIO register, зовнішній assembler symbol чи ручне assume. Sus-код не заборонений автоматично: він просто не має маскуватися під звичайний безпечний Axiom.