Проверка правила словами: digit rule-check

Человек дописывает правило к существующему расчёту по-русски. Правила разбора (без модели) переводят фразу в спецификацию FTS, настоящий компилятор её компилирует и исполняет, детектор fts-gate ищет структурные дефекты вывода — и ответ различает три исхода, а не два.

digit rule-check SPEC.fts "утверждение" ["ещё утверждение" …]

Исходов проверки три; четвёртая строка — не исход, а признание, что проверка не запускалась вовсе, и у неё свой код именно поэтому.

Третий исход — не разновидность второго. «Не понял» и «понял, и это неверно» — разные утверждения, и склеенные они лгут в обе стороны.

Спецификация обязательна и стоит первой

Разбор идёт только над объявленной схемой: поля и их типы — вход, а не то, что восстанавливается из текста. Голое «если сумма больше 1000, скидка 10 %» без известных полей команда не принимает — и не проверкой, а грамматикой.

Причина простая: без объявленного «сумма» любое прочтение этого слова — догадка о том, что такое сумма. Ровно то условие, при котором слой измерялся, и есть условие, при котором его числа что-то значат.

Три исхода на живых прогонах

Все три получены на шаблоне skills/software-development/fts/templates/discount.fts из репозитория Digit: расчёт скидки с двумя правилами, одним свойством («результат не больше 20 процентов от суммы») и одним примером. Вывод настоящий; сокращены только длинные пути и повторяющийся хвост про границу — он приведён ниже отдельно.

Проверено и верно

$ digit rule-check discount.fts "если сумма не меньше 50000, то добавить 3 процента от поля сумма"

Расчёт: «Рассчитать скидку» (2 объявленных правил, 1 свойств, 1 примеров)

Прочитано так:
  если «сумма» не меньше 50000, то прибавить к результату 3 процента от поля «сумма»

ПРОВЕРЕНО И ВЕРНО — правило встаёт в расчёт без противоречий.
  объявленные примеры расчёта (1) по-прежнему сходятся

Исполнено компилятором на проверочных случаях:
  сумма = 49999, постоянный клиент = False → 4999.900000000001
  сумма = 50000, постоянный клиент = False → 6500

Обратите внимание на блок «Прочитано так»: он печатается до приговора и не по вежливости. Расхождение между задуманным и построенным человек обязан увидеть раньше, чем поверит зелёному.

Проверено и неверно

$ digit rule-check discount.fts "если сумма не меньше 10000, то добавить 25 процентов от поля сумма"

ПРОВЕРЕНО И НЕВЕРНО — упала проверка «свойство», код FTS_UTILITY_PROPERTY.
  нарушено свойство «Скидка ограничена» утилиты «Рассчитать скидку»;
  контрпример: сумма = 10000, постоянный клиент = False

Само по себе «+25 % при сумме от 10 000» безупречно. Неверно оно только в паре с объявленным потолком в 20 %, и поэтому правило проверяется в контексте расчёта: объявленные правила, свойства и примеры утилиты едут в проверку вместе с новым правилом. Правило, проверенное в одиночку, получало бы зелёный ровно тогда, когда оно ломает расчёт.

Не удалось формализовать

$ digit rule-check discount.fts "хорошим клиентам надо давать скидку побольше"

НЕ УДАЛОСЬ ФОРМАЛИЗОВАТЬ — приговора не будет.
  • «хорошим клиентам надо давать скидку побольше»
    NO_FRAME: не нашлось рамки «условие → следствие»
  объявленные поля расчёта: «сумма» (Деньги), «постоянный клиент» (Признак)

Догадка здесь была бы хуже отказа: она пришла бы с видом проверенной.

Отказ здесь и есть цена, которой слой платит за ноль тихих ошибок.

Граница печатается в каждом ответе, включая зелёный

Граница: проверено ПОСТРОЕНИЕ правила и его согласованность — типы, покрытие,
границы, отсутствие структурных дефектов вывода. НЕ проверено, верна ли сама
посылка: у системы нет модели мира. Правило «НДС 20 % на экспорт» прошло бы
эти же проверки и получило бы такой же зелёный ответ.

Это не оговорка юриста, а свойство формального слоя: FTS гарантирует «если посылки верны — вывод верен», и истинность объявленного закона является предпосылкой, а не теоремой. На пример с экспортным НДС заведён отдельный тест: если он однажды покраснеет, значит системе приписали модель мира, которой у неё нет.

Подробнее об этом пределе — на странице «Как устроена проверяемость», раздел «Предел формального слоя».

Что нужно, чтобы проверка состоялась

Компилятор FTS и детектор логических ошибок — внешние процессы, и это осознанно: вторая копия компилятора была бы второй реализацией семантики FTS, а вся затея держится на том, что она одна.

Без них команда не деградирует до догадки, а отказывает с путём и именем переменной:

$ digit rule-check discount.fts "если сумма заказа больше 1000, то прибавить 100"
ПРОВЕРИТЬ НЕЧЕМ — детектор логических ошибок: нет …/fts-gate/dist/src/gate.js
(поставить `digit mcp install fts-gate` либо указать DIGIT_FTS_GATE_HOME);
компилятор FTS: нет …/@digitable/fts/dist/src/parser.js (он приезжает вместе с
fts-gate; своя сборка — DIGIT_FTS_HOME)

Код возврата — 4. Ветки «ответить без проверки» у слоя нет по устройству.

Компилятор приезжает зависимостью гейта, поэтому переменная одна и та же:

digit mcp install fts-gate            # обычный путь
export DIGIT_FTS_GATE_HOME=/путь      # своя сборка

Полезные флаги

• --fts — напечатать саму спецификацию, которая была скомпилирована;
• --json — весь результат машиночитаемо: прочтение, приговор, примеры, граница;
• --utility ИМЯ — какую утилиту расширяем; требуется, только если спецификация объявляет больше одной;
• --category ИМЯ — переопределить заголовок категории.

Несколько утверждений принимаются за один прогон: правила и свойства можно передать подряд.

Что измерено

Площадка digit-ml, 1 161 замер:

• формализовано на незнакомых формулировках: 70,6 % при первом открытии holdout и 97,7 % после починки двух системных дыр, которые тот же holdout и нашёл;
• тихих ошибок ноль во всех трёх условиях. Ни одного случая «построилось, компилятор принял, а означает не то». Меряется дифференциальным исполнением: разобранное и эталонное правило исполняет один и тот же интерпретатор на векторах, построенных из порогов обеих сторон;
• детектор логических ошибок: 1 698 порч из 1 698 пойманы, ложных отказов 0 на 394 чистых;
• медиана разбора — около 1 мс.

Тождественность перенесённого в Digit слоя проверена, а не заявлена: измерительный харнесс прогнан против именно этого пакета и дал те же числа (A 394/394, C 382/394, Ch 385/394, чувствительность измерителя 1 778/1 778). Файлы разбора и печати перенесены дословно, байт в байт — sha256 совпадает с оригиналом; изменённые места перечислены в digit_cli/claimcheck/NOTICE.

Границы

Слой отвечает на вопрос «следует ли это из объявленного», а не «правда ли это». Он не знает предметной области, не проверяет закон и не заменяет ревью человека — единственная точка, где решается предметная истинность, находится за пределами формализма.

Цена копии в дерево названа прямо: расхождение с экспериментальной площадкой теперь возможно, синхронизация ручная.

Справочная запись по флагам есть и в английской документации; устройство, числа и границы описаны здесь. Про сам язык FTS — раздел портала.