Executable specifications in flang Toolchain: CLI, WebAssembly, MCP, and JSON
0%

Toolchain: CLI, WebAssembly, MCP, and JSON

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 flang process, a printed module and MCP in one phrase: one compiler, three ways to call it.
  • I find types, functions and examples in flang ast without reading the source.
  • I check results by the exit code and do not count code 3 as success.

Catalogue cases on this topic

Next: Russian and English

Spotted a mistake? Select a fragment of the text — a bug icon will appear next to it.

Нужен разбор именно вашей ситуации?

Статья описывает общий случай. Если у вас частный — можно разобрать его отдельно, платно. А если не хватает целого материала, предложите тему: её оплачивают вскладчину, и она выходит открытой для всех.

Доска запросов
Next