Факт-чекинг: право ответить «не могу проверить»

Режим facts упоминался в этом треке трижды: в главе «Два класса программ» — как причина, по которой язык вообще поделён надвое; в главе «Инструмент» — как одна из шести команд; в главе «Тотальность» — как то, ради чего терпят консервативный анализ. Пора разобрать его целиком, потому что это единственная прикладная поверхность языка: всё остальное в репозитории — устройство, а не применение.

Задача

Есть утверждение. Оно пришло снаружи — из ответа языковой модели, из строки в отчёте, из пункта регламента, от человека в переписке:

«Клиенту положена скидка».

И есть данные, которые лежат у вас: суммы заказов, порог, признак постоянного клиента. Вопрос: подтверждается утверждение этими данными или нет — и, что важнее, можно ли на ответ опереться.

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

Три входа

$ node flang/bin/flang.mjs facts факты.flang \
    --facts факты.json \
    --claims '["«Сумма больше порога» от суммы, порог равно да"]' --pretty

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

модуль «Проверка суммы»

тотальная функция «Сумма списка»
  принимает элементы: список числа
  возвращает число
  пример «Три числа»
    дано элементы равно [10, 20, 30]
    ожидается 60
  разбор элементов
    случай пусто
      то 0
    случай голова и хвост
      то голова плюс «Сумма списка» от хвоста

тотальная функция «Сумма больше порога»
  принимает суммы: список числа, порог: число
  возвращает признак
  пример «Набрал»
    дано суммы равно [10, 20]
    дано порог равно 25
    ожидается да
  пример «Не набрал»
    дано суммы равно [1, 2]
    дано порог равно 10
    ожидается нет
  («Сумма списка» от суммы) больше порог

Функция «Сумма списка» тотальна по канонической схеме из главы «Тотальность»: рекурсия идёт по хвост, пришедшему из образца, то есть по строго меньшей части аргумента. Ту же сумму можно было взять готовой из стандартной библиотеки (глава «Стандартная библиотека») — здесь она выписана, чтобы программа читалась одним файлом.

Второй вход — факты, обычный JSON:

{
  "суммы": [1200, 800, 400],
  "порог": 2000,
  "постоянный": true
}

Форма значений — та же, что у интерпретатора (глава «Интерпретатор»): список это массив, запись это объект, признак это true/false. Совпадение формы не случайно — благодаря ему факт, --args команды run и значение примера внутри функции читаются одним и тем же кодом.

Третий вход — утверждения, строки. Каждая имеет вид <терм> <оператор> <терм>, и в ответе появляется по одной записи на каждую.

Ответ

{
  "ok": true,
  "results": [ {
    "claim": "«Сумма больше порога» от суммы, порог равно да",
    "holds": true,
    "why": "«Сумма больше порога» от факта «суммы», факта «порог» = да;
            требование «равно да» выполнено",
    "status": "verified"
  } ]
}

2400 больше 2000, утверждение подтверждается. Теперь спросим обратное — то же самое, но с ожиданием нет:

{
  "ok": false,
  "results": [ {
    "claim": "«Сумма больше порога» от суммы, порог равно нет",
    "holds": false,
    "why": "«Сумма больше порога» от факта «суммы», факта «порог» = да;
            требование «равно нет» не выполнено",
    …
  } ]
}

Обратите внимание на поле why в обоих случаях: оно называет вычисленное значение и предъявленное требование отдельно. Это не форматирование ради красоты. Ответ «не выполнено» без вычисленного значения оставляет спорящего ни с чем; ответ с числом переводит спор из «инструмент неправ» в «данные не те» или «правило не то» — то есть в разговор, у которого есть исход.

И третий, самый интересный ответ — из главы «Два класса программ», где утверждение опиралось на функцию без пометки тотальная:

{
  "ok": false,
  "results": [ {
    "claim": "«Обратный счёт» от н равно 3",
    "holds": false,
    "why": "функция «Обратный счёт» не помечена как «тотальная»;
            факт-чекинг допускает только тотальные функции —
            иначе ответ может не наступить",
    "status": "refused"
  } ]
}

Здесь holds: false, но означает это совсем не то, что в предыдущем примере.

Три исхода, а не два

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

Отказ бывает по разным причинам, и все они — один класс «не могу»:

• функция, на которую ссылается утверждение, не помечена тотальная (или тотальна не она, а кто-то из вызываемых ею — проверяется транзитивно);
• имени функции нет в программе;
• в фактах нет поля, на которое ссылается терм;
• типы не сходятся: в факте строка, а параметр объявлен числом;
• сама строка утверждения не разобралась по грамматике.

Каждая обязана назвать причину. Формулировка из шапки flang/src/factcheck.mjs, приведённая в главе про два класса, стоит того, чтобы повторить её здесь: «Не „попробуем и посмотрим“: попытка исполнить нетотальную функцию и есть тот риск, ради которого введены два класса».

Грамматика утверждений и почему она такая узкая

Термов четыре вида (flang/src/factcheck.mjs, разбор в главе «Инструмент»):

Операторов шесть: равно, не равно, больше, меньше, не больше, не меньше — и их английские аналоги.

Всё. Ни скобок, ни арифметики в утверждении, ни двух сравнений подряд, ни «и» между ними.

Напрашивается вопрос: почему бы не разрешить в утверждении выражение языка? Синтаксис есть, парсер есть, тайпчекер есть — казалось бы, режим стал бы вдвое полезнее за час работы.

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

• тотальность пришлось бы доказывать на лету, для каждого утверждения отдельно, вместо одной проверки замыкания вызовов по уже проверенной программе;
• утверждение перестало бы быть данными. Сейчас его можно записать в журнал, показать пользователю, сравнить с прошлым, положить в тест. Выражение с локальными связываниями и разбором вариантов — это программа, и обращаться с ней надо как с программой;
• граница ответственности размылась бы. Сейчас правила — ваши, утверждение — чужое, и понятно, кто за что отвечает. С произвольным выражением автор утверждения становится соавтором правил, ничего об этом не зная.

Узость грамматики — не недоделка, а та же цена, которую платит весь язык: выразительность обменивается на проверяемость. В главе «Система типов» так же поступили с функциями высшего порядка, в главе «Тотальность» — с рекурсией по числу.

Что делать, когда утверждение не выражается

Из узости следует практическое правило, и оно неожиданно приятное:

Вся логика живёт в программе, в утверждении остаётся только применение.

Пример. Нужно проверить: «скидка положена, потому что клиент постоянный и набрал на две тысячи». Логических связок в языке нет вовсе (глава «Чего в языке пока нет»), и в утверждении их не появится. Значит, конъюнкция уезжает в функцию, где вместо неё вложенные если:

тотальная функция «Скидка положена»
  принимает суммы: список числа, порог: число, постоянный: признак
  возвращает признак
  пример «Постоянный и набрал»
    дано суммы равно [1200, 800, 400]
    дано порог равно 2000
    дано постоянный равно да
    ожидается да
  пример «Набрал, но не постоянный»
    дано суммы равно [1200, 800, 400]
    дано порог равно 2000
    дано постоянный равно нет
    ожидается нет
  если постоянный равен да
    то («Сумма списка» от суммы) больше порог
    иначе нет

Утверждение снова становится однооператорным:

«Скидка положена» от суммы, порог, постоянный равно да

Посмотрите, что при этом произошло с правилом. Оно:

• тотально — то есть допущено к факт-чекингу;
• снабжено примерами, которые прогоняются командой flang test вместе со всем остальным;
• напечатается в C, Go, JavaScript, Rust или Python (глава «Кодогенерация»), если понадобится считать ту же скидку внутри продукта, а не только проверять утверждения о ней;
• лежит в одном месте. Правило, размазанное по строкам утверждений, не имеет ни автора, ни тестов, ни истории изменений.

Ограничение вытолкнуло логику туда, где ей и место. Это тот же эффект, что в главе «Ядро FTS на flang»: анализ тотальности не запретил написать парсер со спуском, он заставил спускаться по структуре, а не по позиции в потоке — и программа от этого стала лучше.

Почему нельзя было обойтись лимитом шагов

Возражение, которое стоит разобрать: у интерпретатора есть предел шагов (глава «Интерпретатор», миллион по умолчанию, флаг --steps). Зациклившаяся функция упрётся в него за доли секунды и вернёт FLANG_RECURSION_LIMIT. Зачем тогда вообще отказывать нетотальным?

Затем, что лимит защищает от вечности, но не даёт детерминированности.

Функция, укладывающаяся в миллион шагов на сегодняшних данных, не обязана уложиться на завтрашних. Ответ «не знаю» тогда придёт не на сборке, а в проде — и на одних входах утверждение будет проверяться, а на других, внешне похожих, отказывать. Хуже того, полученный так отказ ничего не говорит о правиле: он говорит о размере входа, то есть о случайном обстоятельстве.

Отказ по классу устроен иначе. Он приходит до вычисления, зависит только от текста программы и потому одинаков всегда. Разница ровно та же, что между ошибкой компиляции и ошибкой во время работы, — и выбрана она по той же причине, по которой её выбирают в языках с типами.

Обратное тоже верно, и в репозитории это записано прямо. Компилятор flang, который сейчас переписывается на самом flang, тотальным быть не обязан — он имеет право упереться в лимит шагов и честно об этом сказать, потому что обещает «разобрать или отказать», а не «ответить». Разбор этой асимметрии — в разделе «Кому тотальность обязательна, а кому нет» главы «Два класса программ». Пометка тотальная — не знак качества, а обязательство перед вызывающим, и факт-чекинг — то место, где это обязательство действительно взято.

След как артефакт, а не как отладочный вывод

В ответе есть массив steps — след разбора утверждения, проверки тотальности и вычисления. В главе «Инструмент» сказано, что это не отладочный вывод, а часть смысла режима. Стоит объяснить, откуда такая строгость.

У следа три разных потребителя.

Человек, который не согласен с ответом. Ему нужно не «нет», а «вот из каких фактов и по какому правилу получилось нет». Без следа спор упирается в доверие к инструменту, а доверие — плохое основание для решения о деньгах.

Журнал. Через год вопрос «почему тогда отказали» задаётся всерьёз, и единственный честный ответ — сохранённый след вместе с версией правил. Ответ «так посчитала система» ответом не является.

Тест. Раз why и steps попадают в журналы и на экраны, они — наблюдаемое поведение, а не украшение. Ровно поэтому в главе «Как читать репозиторий» записано, что коды и тексты диагностик копируются буквально, вплоть до кавычек-ёлочек: изменение текста ошибки — изменение поведения.

Встраивание

Контракт вывода — тот же, что у остальных команд: JSON в stdout, ненулевой код возврата при ok: false. Отсюда две готовые схемы применения.

В сборке. Утверждения лежат файлом рядом с правилами, шаг проверки падает, если хоть одно перестало подтверждаться. Это превращает набор утверждений в регрессионный тест на бизнес-правила: поменяли порог — узнали сразу, какие обещания перестали быть правдой.

В агентском конвейере. Модель формулирует утверждение, инструмент отвечает. Разделение труда здесь честное: модель хорошо формулирует и плохо считает, язык хорошо считает и ничего не формулирует. Отказ в таком конвейере — не поражение, а сигнал: спросили о том, чего в правилах нет. Дописать правило дешевле, чем принять правдоподобный ответ модели за проверенный. Про то, зачем вообще проверять ответ агента отдельным механизмом, — глава «Проверка результата» трека про ИИ-агентов.

Ограничение, о котором стоит сказать прямо: факты вы готовите сами. Язык чистый, ни ввода-вывода, ни сети, ни времени в нём нет и не будет (глава «Стандартная библиотека»). Режим встраивается там, где данные уже собраны кем-то другим, и не годится как «спроси у базы».

Чем это отличается от остальных способов

Две строки в этой таблице стоит прочитать вместе. Языковая модель отвечает всегда — и именно поэтому её ответ нельзя отличить от знания. flang facts отвечает не всегда, зато различие между «нет» и «не могу» у него первого класса. Ценность режима не в том, что он умеет больше, а в том, что он умеет ровно столько, сколько может доказать.

Строка про FTS объясняет, откуда режим взялся исторически: в FTS уже были исполняемые предметные правила, но не было ни строк как данных, ни списков, ни рекурсии (глава «flang и FTS»). Факт-чекинг поверх FTS упирался бы в те же стены, что и переписывание ядра.

Цена

Перечислим честно, как весь трек.

• Правила надо написать заранее — и на языке, которому сутки. Если правила меняются чаще, чем поступают утверждения, режим не окупится.
• Факты надо подготовить. Ни одного встроенного способа их достать нет.
• Грамматика узкая, и «сложные» утверждения приходится переносить в функции. Это полезно, но это работа.
• Составное утверждение не выразить без заведения функции под каждое сочетание условий.
• Пользователей за пределами репозитория нет, и разбирать вам придётся самостоятельно.

Область применимости из этого списка следует прямо: режим для случая, когда правила стабильнее утверждений. Тарифы, допуски, регламенты, условия скидок, критерии соответствия — там правило живёт годами, а утверждений о нём проходят тысячи. Для проверки произвольных высказываний о мире он не годится и не притворяется.

Что здесь стоит унести

Даже если flang вы больше никогда не откроете, четыре вещи переносятся куда угодно.

1. Система, обязанная отвечать, обязана уметь отказаться. Ответ, который всегда есть, — это ответ, которому нельзя доверять.
2. Отказ несёт причину и не равен отрицанию. «Нет» и «не знаю» — два разных ответа, и смешивать их дороже всего именно тогда, когда решение важное.
3. Проверяемость покупается сужением. Узкая поверхность ввода — не бедность, а условие, при котором о ней вообще можно что-то доказать.
4. Логику держите в проверяемом коде, а не в строке запроса. Правило, размазанное по формулировкам вопросов, не имеет ни тестов, ни автора, ни истории.

Что дальше

Трек закончен. Четырнадцать глав разбирали язык, которому на момент написания была примерно сутки: откуда он вырос, зачем поделён надвое, как устроены его типы, анализ завершаемости, интерпретатор и пять бэкендов, что уже переписано на нём самом — ядро FTS целиком и пять слоёв компилятора, — чего в языке нет и как в этом разбираться дальше.

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

Куда идти дальше:

• К предшественнику — FTS: язык исполняемых спецификаций, из которого flang вырос, и требования, проверяемые до реализации.
• К устройству языков вообще — Компиляторы и языки: лексер, парсер, типы и кодогенерация в учебном изложении, после которого исходники flang/src/ читаются заметно легче.
• К проверке того, что делает агент — ИИ-агенты, особенно проверка результата и режимы отказов.
• К рассуждению как таковому — Логика и аргументация: чем подтверждение отличается от неопровержения и почему «не знаю» — полноценный ответ.
• К проверкам в конвейере — Тестирование: тест, который не может упасть, ничего не проверяет — та же мысль, с другой стороны.

Общая карта треков портала — в дорожной карте.

И последнее, что повторялось в этом треке чаще остального. Всё написанное сверено на 4 августа 2026 года, коммит ab107c9, — это третья сверка трека за сутки, и наверняка к моменту чтения что-то снова стало неправдой. Проверяйте запуском: node flang/bin/flang.mjs check файл.flang работает без установки и без сборки, отвечает за секунды и не врёт.