Executable specifications: a rule the compiler checks

Take an ordinary requirement: “a regular customer gets another 5%, but the discount may not exceed 15,000 ₽”. Today it lives in three places: as text in a ticket, as branches in code, as test cases with QA. Sometimes in a fourth — in a preview on the frontend. Six months later these versions drift apart, and nobody knows which one is right.

This course is about writing such a rule once — in flang — and getting from the compiler what a ticket’s text cannot give.

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

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

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

The file is checked with two commands:

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

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

Four things happened in those two commands that ordinary code does not give you:

1. Termination is proved. The word тотальная is an obligation: the compiler will not accept the file until it proves the function stops on every input. A rule run in CI, in an operation guard or inside an agent cannot hang.
2. The examples ran. They live inside the function, not in a neighbouring file that someone forgets to update.
3. The types are checked. The amount is declared неотрицательное (non-negative): a negative amount cannot be passed in.
4. The rule reads like it was stated. «Рассчитать скидку», покупка.«сумма» are names from the domain, not calcDiscount(p.amt).

The обеспечивает lines are promises about the result. Which of them are proved is told by a third command (here and below — an excerpt of the report):

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

The first promise is proved for every amount. The second is not: “сетка 2” means it was checked only on the two examples. The compiler does not derive inequalities with percentages, and it says so plainly, with exit code 3. The course teaches you to read this report and not to mistake code 3 for “all good”.

Where the value appears

The value is not that the syntax is shorter than TypeScript. It is in a single checkable source of a domain decision.

The rule, its promises and its reference examples live together in one file. Everyone takes what they need from it: the backend prints it into its own language (flang emit), the frontend reads the structure (flang ast), CI runs the examples on every commit, an agent proposes a change and hands it to the same compiler.

Nothing is left to drift apart: there is one version, and it is executable.

Where this approach is not needed

Do not move the whole application into the specification. A React loop, an SQL query, HTTP client retries, a transaction and sending an email stay ordinary code. A good boundary looks like this:

1. the application reads the data;
2. the rule takes a snapshot of the data and computes a decision;
3. the application checks the result;
4. and only then performs the external effect.

If the rule cannot be made deterministic, or it is simpler to express in three lines that are never duplicated, a specification is unnecessary.

If you have .fts models

The language had an earlier surface — .fts files with the words категория, утилита, правило, свойство. Today’s compiler parses such a file but does not execute its rules and examples, and answers green. The whole course is written in today’s flang; how to port an old model is in the chapter «Older models».

Try it without installing anything

The compiler is built for WebAssembly and runs right on the language page. The model from any chapter opens in the sandbox and is checked at once: types, termination, examples and the proof report.

When it comes to real work, the language installs with one command and runs without Node:

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

On macOS and Linux there is also Homebrew: brew install digitable-lol/tap/flang-package.

The course repository holds working projects: an HTTP discount service, an agent command guard based on facts, TypeScript generation with a drift check in CI, a form schema for the frontend, and clients in Python, Go and shell. The tests of all projects run with one command, npm run spec:examples.

Course route

The course goes from the mechanics of the language to production questions.

Language and model

1. The model and the limits of the language.
2. Tools and JSON.
3. Russian and English notation.
4. Objects and types.
5. Rules and promises.
6. Examples as a new kind of unit test.
7. Reading compiler errors.

Integration

8. Node.js and HTTP.
9. React and forms.
10. Integration with any language.
11. One run and visualization.
12. Generation and CI.

Architecture and team work

13. DDD and command guards.
14. Antipatterns: what not to express in a specification.
15. Migration: from nested ifs to a specification.
16. Rule versions, snapshots and retroactive audit.
17. You don’t need lodash — but not where you think.

Verifiability and limits

18. AI agents and MCP.
19. Proofs and their limits.
20. Requirements checked before implementation.
21. Performance.

End-to-end project

22. Order fulfilment: from the model to the service and the form.

A practical success criterion: after the course you can take one real rule of your project, write it as a total function with promises and examples, read the proof report and wire the result in, without dragging effects into the specification language.

Catalogue cases on this topic

Next: the model and the limits of the language