Исполняемая спецификация: зачем правило, которое компилятор проверяет

Возьмите обычное требование: «постоянный клиент получает ещё 5 %, но скидка не может превысить 15 000 ₽». Сейчас оно живёт в трёх местах: текстом в задаче, ветвлениями в коде, тест-кейсами у QA. Иногда в четвёртом — в предпросмотре на фронтенде. Через полгода эти версии расходятся, и никто не знает, какая из них правильная.

Курс про то, как записать такое правило один раз — на flang — и получить от компилятора то, чего текст в задаче дать не может.

модуль «Скидки»

объект «Покупка»
  «сумма»: неотрицательное

тотальная функция «Рассчитать скидку»
  принимает покупка: «Покупка»
  возвращает число
  обеспечивает «за мелкую покупку скидки нет» если покупка.«сумма» меньше 10000 то результат равен 0 иначе да
  обеспечивает «скидка не больше пятой части суммы» результат не больше (покупка.«сумма» делить на 5)
  пример «мелкая покупка — без скидки»
    дано покупка равно запись «Покупка» с «сумма» равным 1000
    ожидается 0
  пример «от десяти тысяч — десять процентов»
    дано покупка равно запись «Покупка» с «сумма» равным 20000
    ожидается 2000
  если покупка.«сумма» не меньше 10000
    то покупка.«сумма» делить на 10
    иначе 0

Файл проверяется двумя командами:

$ flang check discount.flang
модуль «Скидки»: функций 1, из них с доказанным завершением 1; типов 1
discount.flang: проверено — разбор, типы, завершаемость, ядро и примеры; замечаний нет

$ flang test discount.flang
discount.flang: примеров 2, прошло 2, не прошло 0

За эти две команды произошло четыре вещи, которых обычный код не даёт:

Доказано завершение. Слово тотальная — обязательство: компилятор не примет файл, пока не докажет, что функция останавливается на любом входе. Правило, которое исполняют в CI, в допуске операции или внутри агента, не может зависнуть.
Прогнаны примеры. Они лежат внутри функции, а не в соседнем файле, который забудут обновить.
Проверены типы. Сумма объявлена неотрицательное: отрицательную сумму в функцию не передать.
Правило читаемо тем, кто его формулировал. «Рассчитать скидку», покупка.«сумма» — имена из предметной области, а не calcDiscount(p.amt).

Строки обеспечивает — обещания о результате. Что из обещанного доказано, говорит третья команда (здесь и дальше — выдержка из отчёта):

$ flang check discount.flang --proof
  постусловие «за мелкую покупку скидки нет» функции «Рассчитать скидку» — доказано сведением цели с телом функции: правило «разбор цели по условию», объявленные типы аргументов не понадобились — утверждение обо ВСЕХ входах, а не о написанных; теоремы при нём нет и не нужно
  постусловие «скидка не больше пятой части суммы» функции «Рассчитать скидку» — сетка 2 значения (примеры функции): нарушений НЕ ИСКАЛИ — прогона примеров не было, посчитано только их число. Это не доказательство — теоремы при утверждении нет
discount.flang: НЕ ДОКАЗАНО — ОПОРА НЕ СУДИЛАСЬ — утверждений 2: доказано 1, условно 0, сетка 1, объявлено, не доказано 0, отвергнуто 0, нарушено 0; законов на сетке 0, на веру 0 — код возврата 3

Первое обещание доказано для всех сумм. Второе — нет: «сетка 2» значит, что оно проверено только на двух примерах. Компилятор не выводит неравенства с процентами, и он говорит об этом прямо, кодом возврата 3. Курс учит читать этот отчёт и не принимать код 3 за «всё хорошо».

Где появляется ценность

Ценность не в том, что синтаксис короче TypeScript. Она в одном проверяемом источнике предметного решения.

Правило, обещания и контрольные примеры лежат рядом, в одном файле. Дальше каждый берёт из него своё: бэкенд печатает его в свой язык (flang emit), фронтенд читает структуру (flang ast), CI гоняет примеры на каждый коммит, агент предлагает изменение и отдаёт его тому же компилятору.

Расходиться становится нечему: версия одна, и она исполняемая.

Где этот подход не нужен

Не переносите в спецификацию всё приложение. Цикл React, SQL-запрос, retry HTTP-клиента, транзакция и отправка письма остаются обычным кодом. Хорошая граница выглядит так:

приложение читает данные;
правило принимает снимок данных и вычисляет решение;
приложение проверяет результат;
и только затем выполняет внешний эффект.

Если правило невозможно сделать детерминированным или его проще выразить тремя строками, которые никогда не дублируются, спецификация будет лишней.

Если у вас есть модели `.fts`

У языка была ранняя поверхность — файлы .fts со словами категория, утилита, правило, свойство. Сегодняшний компилятор такой файл разбирает, но правил и примеров в нём не исполняет и отвечает зелёным. Весь курс написан на сегодняшнем flang; как перенести старую модель — в главе «Старые модели».

Попробовать, ничего не устанавливая

Компилятор собран в WebAssembly и работает прямо на странице языка. Модель из любой главы открывается в песочнице и сразу проверяется: типы, завершение, примеры и отчёт о доказательствах.

Когда дойдёт до дела, язык ставится одной командой и работает без Node:

curl -fsSL https://raw.githubusercontent.com/digitable-lol/flang/main/install.sh | sh
flang check ваше-правило.flang

На macOS и Linux есть и Homebrew: brew install digitable-lol/tap/flang-package.

В репозитории курса лежат рабочие проекты: HTTP-сервис расчёта скидки, допуск команды для агента по фактам, генерация TypeScript с проверкой расхождения в CI, схема формы для фронтенда и клиенты на Python, Go и shell. Тесты всех проектов запускаются одной командой npm run spec:examples.

Маршрут курса

Курс идёт от механики языка к производственным вопросам.

Язык и модель

Интеграция

Архитектура и работа команды

Проверяемость и границы

Сквозной проект

Исполнение заказа: от модели до сервиса и формы.

Практический критерий успеха: после курса вы умеете выбрать одно реальное правило своего проекта, оформить его тотальной функцией с обещаниями и примерами, прочитать отчёт о доказательствах и встроить результат, не перетаскивая эффекты в язык спецификации.

Кейсы каталога по этой теме

Каталог применимости

Эти кейсы разбирают тему главы:

Сельское хозяйство