Executable specifications: a rule the compiler checks
Take an ordinary requirement: “a returning customer gets another 5 %, but the discount may not exceed 15 000 ₽”. Right now it lives in three places: as text in the ticket, as branching in the code, as test cases at QA. Sometimes in a fourth — the preview on the frontend. Half a year later those versions have drifted 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 text in a ticket cannot give.
объект «Покупка»
«сумма»: число
«постоянный клиент»: признак
тотальная функция «Рассчитать скидку»
принимает покупка: «Покупка»
возвращает число
обеспечивает «скидка не больше двадцати процентов» результат не больше (покупка.«сумма» делить на 5)
пример «мелкая покупка — без скидки»
дано покупка равно запись «Покупка» с «сумма» равным 1000 и «постоянный клиент» равным нет
ожидается 0
пример «от десяти тысяч — десять процентов»
дано покупка равно запись «Покупка» с «сумма» равным 20000 и «постоянный клиент» равным нет
ожидается 2000
если покупка.«сумма» не меньше 10000
то покупка.«сумма» делить на 10
иначе 0The file is checked by a single command, and here is what it answers:
$ flang check skidka.flang
без имени модуля: функций 1, из них с доказанным завершением 1; типов 1
skidka.flang: проверено — разбор, типы, завершаемость, ядро и примеры; замечаний нет
$ flang test skidka.flang
skidka.flang: примеров 2, прошло 2, не прошло 0
Four things happened in those two commands, and ordinary code gives none of them:
- Termination is proved. The word
тотальнаяis an obligation: the compiler will not build the file until it proves the function halts on every input. A rule that runs in CI, in an operation gate or inside an agent cannot be allowed to hang. - The postcondition is checked. The
обеспечиваетline is not a comment: it is a statement about the result, and it is checked rather than assumed. - The examples were run. They live inside the function, not in a neighbouring file somebody forgets to update.
- The rule reads for the person who stated it.
«Рассчитать скидку»,покупка.«сумма»— names from the domain, notcalcDiscount(p.amt).
Where the value comes from
The value is not that the syntax is shorter than TypeScript. It is one verifiable source for a domain decision.
Rule, postcondition and control examples sit together, in one file. From there each side takes its own: the backend runs it directly or prints it into its own language, the frontend reads the structure, CI executes the examples on every commit, an agent proposes a change and hands it to the same compiler — which either proves it or refuses.
There is nothing left to drift: there is one version, and it is executable.
Where this approach is not needed
Do not move the whole application into a specification. The React loop, the SQL query, the HTTP client’s retry, the transaction and the outgoing email stay ordinary code. A good boundary looks like this:
- the application reads the data;
- the rule takes a snapshot of it and computes a decision;
- the application checks the result;
- and only then performs the external effect.
If a rule cannot be made deterministic, or if three lines that never get duplicated express it better, a specification will be redundant.
What to know about the earlier surface of the language
This course was written when the language had an early surface — with the words
категория, объект, утилита, правило, свойство, and files named
.fts. Some chapters below show examples in exactly that surface.
Today’s compiler still reads those words, but does not treat such a file as a
program: a file holding only utilities is not a program, and flang check
answers with a refusal that names what to use instead (flang/SPEC.md, §9).
Carrying a model over is manual, by the table in the chapter
«Older models», and it is not
hard: examples carry over verbatim, a utility becomes a total function, a
property becomes an обеспечивает line.
A practical hint: read the chapters for how they take a problem apart, and type the code in today’s syntax — the one shown above and taken apart in the «flang» track.
Try it without installing anything
The compiler is built for the browser and runs right on the language page: a rule from any chapter opens in the sandbox, where the parse, the example results, the run and the proof are visible at once. Nothing has to be installed for a first look.
When it comes to real work, the language installs with one command and needs no Node:
brew install digitable-lol/tap/flang
flang check ваше-правило.flang
The course repository carries four working integration projects: an HTTP
discount service, a command gate for an agent backed by a proof, code generation
with a drift check in CI, and a form schema for the frontend. All of them run
with a single npm run fts:examples and are covered by tests.
Course Track
The course moves from language mechanics to production issues.
Language and Model
- Model and language boundaries.
- Installation and canonical JSON.
- Russian and English notation.
- Structures and types.
- Utilities, rules, and properties.
- Examples as a new kind of unit test.
- Reading compiler errors.
Integration
- Node.js and HTTP.
- React and Forms.
- Integration with Any Language.
- Single Run and Visualization.
- Generation and CI.
Architecture and Team Workflow
- DDD and command guards.
- Antipatterns: what should not be expressed in the specification.
- Migration: from nested if to specification.
- Rule versions, snapshots, and retroactive audit.
- You don’t need lodash — but not where you think.
Verifiability and boundaries
- AI agents, Digit and MCP.
- Proofs and certificates.
- Requirements checked before implementation: spec corpus, constitution, and
ftspec. - Performance.
Cross-cutting project
Practical success criterion: after the course you can choose one real rule of your project, write it as a total function, check it with examples and integrate the result, without dragging effects into the specification language.
