Toolchain: CLI, WebAssembly, MCP, and JSON
This chapter is about the tools around the language, not the syntax: how to install the compiler, which commands check a model, and what exactly travels between processes when the rule is needed not only in a terminal but also in Node.js, in the browser and in an AI agent.
Minimal example
модуль «Продажи»
тотальная функция «Скидка»
принимает сумма: неотрицательное, постоянный: признак
возвращает число
обеспечивает «за мелкую покупку скидки нет» если сумма меньше 10000 то результат равен 0 иначе да
пример «мелкая покупка»
дано сумма равно 5000
дано постоянный равно да
ожидается 0
пример «большая покупка постоянного клиента»
дано сумма равно 20000
дано постоянный равно да
ожидается 3000
если сумма не меньше 10000
то (если постоянный то (сумма умножить на 15) делить на 100 иначе (сумма умножить на 10) делить на 100)
иначе 0
The rest of the chapter covers which commands work with it and what each one answers.
What the compiler does
There is one compiler — the flang binary, written in flang itself and built
from C. All commands go through the same checks: parsing, types, termination,
the proof kernel. So flang check in a terminal, the “Check” button in the
sandbox and an agent’s flang_check call answer the same way.
The sandbox on the language page is the same compiler built for WebAssembly. It runs in the browser tab, with no server.
Installation
The language is open — github.com/digitable-lol/flang
— and installs with one command, without sudo:
$ curl -fsSL https://raw.githubusercontent.com/digitable-lol/flang/main/install.sh | sh
$ flang --version
flang 0.7.29
The installer picks the build for your system, verifies its checksum and puts
it into ~/.local. FLANG_VERSION=0.7.29 pins the version, PREFIX chooses
the place. There is also Homebrew: brew install digitable-lol/tap/flang-package.
From source you need only a C compiler and make:
git clone https://github.com/digitable-lol/flang && cd flang
make -C bootstrap -j4
make -C bootstrap install PREFIX=$HOME/.local
LLVM has its own flang — a Fortran compiler. If both are installed, the
first one in PATH wins. Ours prints flang 0.7.29 on the first line of
flang --version.
Commands
| Command | What it does | Exit code |
|---|---|---|
flang check файл |
parsing, types, termination, examples | 0 — no remarks, 1 — remarks |
flang check файл --proof |
the same plus the proof report | 0 — all proved, 3 — not all |
flang test файл |
runs the examples | 0 — all passed |
flang run файл --function «Имя» --args '…' |
evaluates one function | 3 — the program is not proved |
flang emit файл --target язык |
prints the program in another language | 1 — the program failed the check |
flang ast файл |
the parsed program as JSON | 0 |
flang facts файл --facts факты.json --claims '[…]' |
checks claims on facts | 1 — refuted |
flang --mcp-mode |
a service for an AI assistant | — |
flang lsp --stdio |
a language server for the editor | — |
On the example above:
$ flang check sales.flang
модуль «Продажи»: функций 1, из них с доказанным завершением 1; типов 0
sales.flang: проверено — разбор, типы, завершаемость, ядро и примеры; замечаний нет
$ flang test sales.flang
sales.flang: примеров 2, прошло 2, не прошло 0
$ flang run sales.flang --function Скидка --args '{"сумма": 20000, "постоянный": true}'
доказано: утверждений 1
3000
The first line of flang run goes to standard error: it is the verdict about
proofs. The value goes to standard output. A program with unproved promises is
not evaluated by flang run: it exits with code 3 until you consent with the
--trust flag.
flang emit prints the program into one of ten targets: c, cpp, go, rust, java,
js, ts, elixir, python, csharp. The printed code runs without flang:
$ flang emit sales.flang --target python --out printed
проверок при работе снято 1: постусловие доказано ядром обо всех входах и
проверено примерами функции — в напечатанный код оно не едет.
напечатано файлов 4, байт 102406, в printed
проверено перед печатью — разбор, типы, завершаемость и ядро доказательств.
ПРИМЕРЫ НЕ ПРОГНАНЫ: их считает вычислитель на самом языке, и на самых больших
программах он в предел шагов этого бинарника не укладывается — свяжи с ними
печать, и компилятор перестал бы печатать сам себя. Прогоните их отдельно:
flang test <файл>
запустить: cd <каталог> && python3 flang_cli.py <модуль>
Note the line about examples: emit does not run them. In a build, flang test
is a separate step before printing.
A trap: files of the earlier surface
A .fts file with the words категория, утилита, правило is accepted by
today’s compiler and answered green, with nothing checked:
$ flang check order-discount.fts
модуль «Продажи»: функций 0, из них с доказанным завершением 0; типов 1
order-discount.fts: проверено — разбор, типы, завершаемость, ядро и примеры; замечаний нет
$ flang test order-discount.fts
flang test: под «order-discount.fts» не нашлось ни одного .flang
Read such an answer by its numbers: функций 0 (zero functions). The utility
did not become a function; the rules and examples did not run. How to port the
model is in the chapter
«Older models».
Three ways to call a rule
A process. CI, shell, Python and Go call flang run or flang facts and
read the answer. The arguments of flang run are flat JSON of scalars. It does
not accept records or lists: for those, the model gets a function with scalar
arguments, or you call flang facts.
A printed module. Node.js and the browser take the module printed by
flang emit --target js or --target ts. It is an ordinary function with no
dependencies and no compiler at runtime. There is no separate JS compiler
library with compile and validate functions any more: the old npm package
@digitable-lol/fts 0.4.7 understands only the earlier surface. How this works
in the course service is in the chapter «Node.js and HTTP».
MCP. An agent gets two tools: flang_check (input source) and
flang_prove (inputs source and claim). Configuration:
{"mcpServers": {"flang-validator": {"command": "flang", "args": ["--mcp-mode"], "env": {}}}}
The source goes as a call argument, not as a file path: the agent gets no access to the file system. There is no “ok” field in the answers. Each promise comes as one of the report’s words — “доказано”, “сетка N”, “объявлено, не доказано” — and the agent cannot retell “сетка” as “proved” without lying.
JSON instead of text
flang has no single “canonical document” of a model, as the former FTS had. There are three machine-readable answers, each with its own job.
flang ast is the parsed program. Its top-level keys: flang (format version),
module, types, functions, legacy. The function from the example (an
excerpt):
$ flang ast sales.flang | jq '.functions[0] | {name, total, examples: [.examples[] | {name, args, expected}]}'
{
"name": "Скидка",
"total": true,
"examples": [
{
"name": "мелкая покупка",
"args": {
"сумма": 5000,
"постоянный": true
},
"expected": 0
},
{
"name": "большая покупка постоянного клиента",
"args": {
"сумма": 20000,
"постоянный": true
},
"expected": 3000
}
]
}
From types the frontend builds a form, from examples — a table of reference
cases. Function bodies are there too, as a tree. You do not need to execute it
yourself: that is what flang emit is for.
flang facts is a verdict on a claim: holds, status (verified or
refuted), why in words and steps — the evaluation steps. It is taken
apart in the chapter
«The model and the limits of the language».
flang test --json is the result of the example run on one line:
$ flang test sales.flang --json | jq '{valid, total, passed, failed}'
{
"valid": true,
"total": 2,
"passed": 2,
"failed": 0
}
JSON-first discipline
Do not look for the word “проверено” in the output — go by the exit code:
if flang check policy.flang --proof && flang test policy.flang; then
echo "правило доказано, примеры сошлись"
else
echo "правило не прошло: смотрите отчёт" >&2
exit 1
fi
Code 3 from check --proof is a failure here too, and on purpose: “checked on
examples” is not “proved”. If the team knowingly accepts an unproved promise,
that decision is written into the build explicitly, not hidden behind || true.
Sandbox practice
Press “Check” and find the only proved promise in the report. Which three rest only on examples?
Add an example to «Рассчитать доставку»: weight 20, distance 100, no urgency and no insurance. Work out the expected number by hand from the functions «Базовый тариф» and «Надбавки» and make the example pass.
Find the function «Скидка по сумме». Why is it needed if «Рассчитать скидку»
exists? A hint: what does --args of flang run accept.
Common mistakes
A record in --args. flang run accepts only a flat object of scalars:
$ flang run sales.flang --function Скидка --args '{"сумма": {"x": 1}, "постоянный": true}'
flang run: «--args» разобрать не удалось — ждался плоский объект скаляров, вроде '{"н":10}'
This is code 2 — a malformed call. The fix is a function with scalar arguments,
or flang facts.
FLANG_TYPE on input. Arguments are checked against the declared types
before evaluation. A string instead of a number gives code 1:
$ flang run sales.flang --function Скидка --args '{"сумма": "много", "постоянный": true}'
доказано: утверждений 1
FLANG_TYPE: вызов функции «Скидка»: аргумент «сумма» не соответствует типу неотрицательное
The course service examples/spec/discount-api answers such input with 400,
not 500: the cause is in the request data, not in the server logic.
Checklist
- I know which command to call for checking, for the examples, for one evaluation and for printing into my language.
- I explain the difference between a
flangprocess, a printed module and MCP in one phrase: one compiler, three ways to call it. - I find types, functions and examples in
flang astwithout reading the source. - I check results by the exit code and do not count code 3 as success.