Исполняемая спецификация: зачем правило, которое компилятор проверяет
Возьмите обычное требование: «постоянный клиент получает ещё 5 %, но скидка не может превысить 15 000 ₽». Сейчас оно живёт в трёх местах: текстом в задаче, ветвлениями в коде, тест-кейсами у QA. Иногда в четвёртом — в предпросмотре на фронтенде. Через полгода эти версии расходятся, и никто не знает, какая из них правильная.
Курс про то, как записать такое правило один раз — на flang — и получить от компилятора то, чего текст в задаче дать не может.
объект «Покупка»
«сумма»: число
«постоянный клиент»: признак
тотальная функция «Рассчитать скидку»
принимает покупка: «Покупка»
возвращает число
обеспечивает «скидка не больше двадцати процентов» результат не больше (покупка.«сумма» делить на 5)
пример «мелкая покупка — без скидки»
дано покупка равно запись «Покупка» с «сумма» равным 1000 и «постоянный клиент» равным нет
ожидается 0
пример «от десяти тысяч — десять процентов»
дано покупка равно запись «Покупка» с «сумма» равным 20000 и «постоянный клиент» равным нет
ожидается 2000
если покупка.«сумма» не меньше 10000
то покупка.«сумма» делить на 10
иначе 0
Этот файл проверяется одной командой, и вот что она отвечает:
$ flang check skidka.flang
без имени модуля: функций 1, из них с доказанным завершением 1; типов 1
skidka.flang: проверено — разбор, типы, завершаемость, ядро и примеры; замечаний нет
$ flang test skidka.flang
skidka.flang: примеров 2, прошло 2, не прошло 0
Четыре вещи произошли за эти две команды, и ни одну из них не даёт обычный код:
- Доказано завершение. Слово
тотальная— обязательство: компилятор не соберёт файл, пока не докажет, что функция останавливается на любом входе. Правило, которое исполняют в CI, в допуске операции или внутри агента, не может зависнуть. - Проверено постусловие. Строка
обеспечивает— не комментарий: это утверждение о результате, и оно проверяется, а не подразумевается. - Прогнаны примеры. Они лежат внутри функции, а не в соседнем файле, который забудут обновить.
- Правило читаемо тем, кто его формулировал.
«Рассчитать скидку»,покупка.«сумма»— имена из предметной области, а неcalcDiscount(p.amt).
Где появляется ценность
Ценность не в том, что синтаксис короче TypeScript. Она в одном проверяемом источнике предметного решения.
Правило, постусловие и контрольные примеры лежат рядом, в одном файле. Дальше каждый берёт из него своё: бэкенд исполняет напрямую или печатает в свой язык, фронтенд читает структуру, CI выполняет примеры на каждый коммит, агент предлагает изменение и отдаёт его тому же компилятору — который либо докажет, либо откажет.
Расходиться становится нечему: версия одна, и она исполняемая.
Где этот подход не нужен
Не переносите в спецификацию всё приложение. Цикл React, SQL-запрос, retry HTTP-клиента, транзакция и отправка письма остаются обычным кодом. Хорошая граница выглядит так:
- приложение читает данные;
- правило принимает снимок данных и вычисляет решение;
- приложение проверяет результат;
- и только затем выполняет внешний эффект.
Если правило невозможно сделать детерминированным или его проще выразить тремя строками, которые никогда не дублируются, спецификация будет лишней.
Что нужно знать про прежнюю поверхность языка
Курс писался, когда у языка была ранняя поверхность — со словами категория,
объект, утилита, правило, свойство и файлами .fts. Часть глав ниже
показывает примеры именно в ней.
Сегодняшний компилятор эти слова читает, но программой такой файл не считает:
файл, где есть только утилиты, — не программа, и flang check отвечает отказом,
называя, чем пользоваться сейчас (flang/SPEC.md, §9). Перенос — ручной, по
таблице соответствий из главы
«Старые модели», и он несложный:
примеры переносятся дословно, утилита становится тотальной функцией, свойство —
строкой обеспечивает.
Практический совет: читайте главы ради разбора задачи, а код набирайте в сегодняшнем синтаксисе — том, что показан выше и разобран в треке «flang».
Попробовать, ничего не устанавливая
Компилятор собран для браузера и работает прямо на странице языка: правило из любой главы открывается в песочнице, где сразу видно разбор, результат примеров, выполнение и доказательство. Для первого знакомства ставить ничего не нужно.
Когда дойдёт до дела, язык ставится одной командой и работает без Node:
brew install digitable-lol/tap/flang
flang check ваше-правило.flang
В репозитории курса лежат четыре рабочих проекта интеграции: HTTP-сервис расчёта
скидки, допуск команды для агента через доказательство, генерация кода с
проверкой расхождения в CI и схема формы для фронтенда. Все они запускаются
одной командой npm run fts:examples и покрыты тестами.
Маршрут курса
Курс идёт от механики языка к производственным вопросам.
Язык и модель
- Модель и границы языка.
- Установка и канонический JSON.
- Русская и английская запись.
- Структуры и типы.
- Утилиты, правила и свойства.
- Примеры как новый вид unit-теста.
- Читаем ошибки компилятора.
Интеграция
- Node.js и HTTP.
- React и формы.
- Интеграция с любым языком.
- Единый прогон и визуализация.
- Генерация и CI.
Архитектура и работа команды
- DDD и command guards.
- Антипаттерны: что не стоит выражать в спецификации.
- Миграция: от вложенных if к спецификации.
- Версии правил, снапшоты и аудит задним числом.
- Вам не нужен lodash — но не там, где вы думаете.
Проверяемость и границы
- AI-агенты, Digit и MCP.
- Доказательства и сертификаты.
- Требования, которые проверяются до реализации: корпус спек, конституция и
ftspec. - Производительность.
Сквозной проект
Практический критерий успеха: после курса вы умеете выбрать одно реальное правило своего проекта, оформить его тотальной функцией, проверить примерами и встроить результат, не перетаскивая эффекты в язык спецификации.