Checking the rule with words: digit rule-check

A person adds a rule to an existing calculation in Russian. The parsing rules (without a model) translate the phrase into an FTS specification; a real compiler compiles and executes it; the detector fts-gate searches for structural defects in the output— and the answer distinguishes three outcomes, not two.

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

There are three possible outcomes of the check; the fourth line is not an outcome, but an acknowledgment that the check was not run at all, and it has its own code for this reason.

The third outcome is not a variation of the second. “I don’t understand” and “I understand, but it’s wrong” are different statements, and when combined, they lie in both directions.

Specification is mandatory and should be placed first.

The walkthrough applies only to the declared schema: fields and their types are the input, not what is reconstructed from the text. A bare “if the sum is greater than 1000, the discount is 10%” without known fields is not accepted by the command — not by a check, but by grammar.

The reason is simple: without an announced “sum,” any reading of this word is a guess as to what a sum is. Precisely the condition under which the layer was measured is the condition under which its numbers mean something.

Three outcomes in live runs

All three were obtained using the skills/software-development/fts/templates/discount.fts template from the Digit repository: discount calculation with two rules, one property (“the result is no more than 20 percent of the total”) and one example. The output is correct; only long paths and the repetitive tail about the boundary have been shortened—it is provided below separately.

Verified and correct

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

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

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

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

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

Note the “Read as follows” block: it is printed before the verdict and not out of politeness. A person is obliged to see the discrepancy between what was intended and what was built before believing the green.

Checked and incorrect

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

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

In itself, “+25% for amounts over 10,000” is flawless. It is only incorrect in combination with the declared limit of 20%, and therefore the rule is checked in the context of the calculation: the declared rules, properties, and examples of the utility go into the check together with the new rule. A rule checked in isolation would receive a green light only when it breaks the calculation.

Failed to formalize

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

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

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

The cost here is the rejection, which is the price the layer pays for zero silent fallacies.

The border is printed in every response, including the green one.

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

This is not a lawyer’s loophole, but a property of the formal layer: FTS guarantees “if the premises are true, then the conclusion is true,” and the truth of the declared law is a premise, not a theorem. A separate test has been created for the example with export VAT: if it turns red, it means that the system has been assigned a world model that it does not have.

More details about this limit can be found on the page “How verifiability works”, section “Limit of the formal layer.”

What is needed for the check to take place

The FTS compiler and fallacy detector are external processes, and this is intentional: a second copy of the compiler would be a second implementation of the FTS semantics, and the whole idea relies on the fact that there is only one.

Without them, the team will not degenerate into guesswork, but will refuse with a path and the name of the variable:

$ 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)

Return code is 4. The layer does not have a “respond without checking” branch by design.

The compiler arrives as a gate dependency, so the variable is the same:

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

Useful Flags

• --fts — print the specification itself, which was compiled;
• --json — the entire result is machine-readable: reading, verdict, examples, boundary;
• --utility ИМЯ — which utility are we extending; required only if the specification declares more than one;
• --category ИМЯ — redefine the category header.

Several statements are accepted for one run: rules and properties can be passed consecutively.

What is measured

Platform digit-ml, 1,161 measurements:

• formalized on unfamiliar formulations: 70.6% upon first opening, holdout, and 97.7% after fixing two system vulnerabilities, which the same holdout also found;
• zero silent errors in all three conditions. Not a single case of “it compiles, the compiler accepts it, but it means something else.” Measured by differential execution: the parsed and reference rule is executed by the same interpreter on vectors constructed from the thresholds of both sides;
• logical fallacy detector: 1,698 corruptions out of 1,698 caught, false positives 0 out of 394 clean ones;
• median parsing time is about 1 ms.

The identity of the layer transferred to Digit has been verified, not just asserted: the measurement harness was run against this specific package and produced the same numbers (A 394/394, C 382/394, Ch 385/394, measurement sensitivity 1 778/1 778). The walkthrough and printing files were transferred verbatim, byte for byte – sha256 matches the original; the modified locations are listed in digit_cli/claimcheck/NOTICE.

Boundaries

The layer answers the question of whether something follows from what has been declared, not whether it is true. It does not know the subject area, does not check the law, and does not replace human review – the only point where subject truth is determined is outside the formalism.

The cost of copying to the tree is stated directly: divergence from the experimental environment is now possible, and synchronization is manual.

There is also a reference entry on flags in the English documentation; the device, numbers, and boundaries are described here. The FTS language itself is described in this portal section.