flang

flang is a programming language with an executable specification. Its distinctive feature is the division of programs into two classes, which the compiler distinguishes: programs for which termination is proven, and all others. The language’s surface is textual: the syntax contains no characters that cannot be typed on a standard keyboard.

The language evolved from FTS (Formal Type Surface) — a language for executable specifications used to describe subject domains. Today these are two surfaces of one project, and they should not be confused.

The binary’s help promises it does not take .fts: “the bridge from FTS („.fts“ models, the laws on top of them) is not accepted by the binary at all” (flang check --help). A run turns out worse than a refusal. flang check parses the model as a program with no functions and prints green with exit code 0 — exactly what it prints for an empty file. flang check --proof spells it out: “no declared functions”, “no declared laws”, and the theorem — “declared, not proven: an old form (FTS legacy)”. A green answer on .fts does not mean it was checked, and it cannot be relied upon.

The FTS delivery channel was closed by the owner’s decision on 31 August 2026. The @digitable-lol/fts package did not vanish: version 0.4.7 sits in the portal’s dependencies, and the vendored copy that runs this section’s playground is built from it. The language is installed by the formula — brew install digitable-lol/tap/flang, binary 0.6.2.

A subject domain is written in flang itself today: that is fspec, and it has its own section below.


Paradigm	functional, declarative
Appeared	August 2026
Typing	static, strong, sum and product types
License	BSD 2-Clause
File extensions	`.flang`, `.fp`, `.фп`, `.фланг`
Repository	digitable-lol/flang

Features

Two classes of programs

The compiler distinguishes between functions with the тотальная attribute, for which termination is proven for any input, and ordinary functions with arbitrary recursion.

The proof proceeds in two ways. Structural descent: each recursive call receives a structurally smaller argument — the tail of the list, the field of a record, the field of a variant. A numeric measure: the argument decreases by a constant step and is bounded from below by an inequality check. What neither of the two accepts is rejected, and this is not nitpicking: размер минус позиция decreases, but it has no constant step — the position grows from turn to turn, and this cannot be used to justify termination without reasoning that the compiler does not perform.

The division has a direct consequence: in the embedded fact-checking mode, only total functions are allowed. A system that answers the question “confirmed or not” is not allowed to hang.

тотальная функция «Длина»
  принимает элементы: список числа
  возвращает число
  разбор элементов
    случай пусто
      то 0
    случай голова и хвост
      то 1 плюс «Длина» от хвоста

Printing in target languages

The program is printed in source code in nine languages: C, C++, Go, Rust, Python, Java, C#, Elixir, and JavaScript.

Printing is accompanied by differential verification: the printed code must produce the same values, the same codes, and the same error messages as the interpreter. For each goal, this is checked on 35 programs, 214 functions, and 3071 grid points of inputs, and the grid is constructed not only from examples but also by corrupting each argument with deliberately foreign values—otherwise, the diagnostics would remain untested.

Such a check reveals defects that are not visible in tests of a single backend. During development, the following were found: printing of non-compilable C code when the name of the variant and the function coincide; a variant literal that turned into an entry in the Go backend; a signed zero when dividing by infinity in Elixir.

Verbal Syntax

In the syntax, only the words из … в …, после, цепочка … сначала … затем …, сохраняет композицию are used. Russian and English are equally valid and are compiled into a single syntax tree.

Categorical surface

Morphism declares an arrow between objects of a category; composition is written with the word после, and a long chain is written in reading order:

морфизм «отгрузить» из «Заказ» в «Отгрузка»
морфизм «выставить» из «Отгрузка» в «Счёт»
морфизм «оформить» это «выставить» после «отгрузить»

цепочка «провести заказ»
  сначала «отгрузить»
  затем «выставить»
  затем «оплатить»

The composition’s alignment is provable from the declarations: «б» после «а» is assembled if and only if the codomain «а» is equal to the domain «б». Misalignment indicates what didn’t align with what:

FLANG_COMPOSE_MISMATCH: «выставить» приводит в «Счёт», а «отгрузить» ожидает «Заказ»

What follows needs a caveat, without which this whole section reads wrongly: the binary compiler today does not judge the rules of the categorical surface at all. It parses the declarations, checks types, termination, proofs and examples, and once it reaches the laws of the surface it names the unchecked parts one by one and exits with code 2 — “not checked TO THE END”, because “no remarks” would read here as “verified”. The judge is not lost, it is not wired in: the layers that compute these laws are written in flang itself (flang/self/monoid.flang, monad.flang, iso.flang, functor.flang), but none of them enters the build of the binary, and the earlier JavaScript implementation that used to compute them has been removed. Everything said below with the word “verified” is the contract of flang/cat/SPEC.md, not today’s answer from the command.

A functor maps objects and arrows, and its three laws relate to what is proven, not to what is verified by examples: the image of an arrow must lead from the image of the domain to the image of the codomain, the image of a composition must be the composition of the images in the same order, and the image of the identity must be the identity of the image. Proof is possible here because a morphism is a declaration, not a value: the domain and codomain are known before execution, and the laws are verified by comparing declarations, without a grid and without a solver. The names of categories remain a label for the reader: a category is not declared as a separate entity, and there is nothing to assert the belonging of an object to it.

A monoid is defined by its carrier, operation, and identity; with an inverse, it becomes a group – there is no separate term for it, because a group is simply a monoid with an inverse. Here, the boundary between “proven” and “verified” lies within a single construct: the structure is proven (the operation is a function of two arguments of the carrier, the identity is a value of the carrier), while the laws themselves – associativity, neutrality, invertibility – are verified on a finite grid of operation examples. They cannot be proven: these are equalities of computations on all values of the carrier.

Isomorphism and bifunctor are declared and verified using the same declaration matching. In the case of isomorphism, the equality “inverse after direct = identity” is not checked at all — neither by proof nor on the grid: a category arrow has no body, there is nothing to compute. This is the author’s assumption, and the compiler only responds to whether it is meaningfully formulated.

A monad is declared over a parametric type and names two functions — возврат and соединение. The endofunctor’s mapping is not declared at all: a polynomial functor has exactly one, and the compiler derives it from the structure of the type. The form в монаде rests on the same ground — do-notation in words, which is unfolded inside parsing into ordinary calls, so all nine targets get it for free (flang/cat/MONAD.md).

Natural transformations are still only described in the contract flang/cat/SPEC.md and are not implemented, but the reason has shifted: what used to block them was parametric polymorphism itself, and now it exists — what blocks them is that the linking of morphisms knows the name of a type, not an application (flang/cat/POLY.md, phase 3).

Analysis of Judgments

In addition to syntax and type errors, the check reports defects in the rules themselves: unreachable properties, gaps in input coverage, and rule overlaps. The analysis is interval-based and precise for conditions comparing a field with a constant; conditions linking fields to each other are honestly marked as unanalyzed.

FTS_COVERAGE_HOLE          при «сумма» ∈ (−∞, 10000) не срабатывает ни одно
                           правило — результат остаётся начальным (0)
FTS_PROPERTY_VIOLATED      свойство «Скидка ограничена» нарушается при
                           «сумма» ∈ (−∞, 0): результат 0 против предела −200000
FTS_PROPERTY_UNATTAINABLE  предел «результат ≤ 20 % от поля «сумма»» не берётся
                           нигде, где правила меняют результат

The diagnostics are provided in JSON format with a code, level, and location, making them suitable for machine parsing, which is crucial for scenarios where the code is not written by a human. But a code with the FTS_ prefix is a property of the earlier surface, and the installed 0.7.3 binary does not print such codes at all: in the compiler’s own sources (flang/self/) the diagnostic codes carry the FLANG_ prefix, not a single one carries FTS_. The three examples above are shown by this page’s playground; there is no tool today that would produce them on your machine.

Implementation

There is one implementation: the flang compiler is written in flang — 118,918 lines in 60 files under flang/self/**. It prints itself and also into eight target languages.

The witness implementation in TypeScript and JavaScript, which used to serve as the definition of the language’s behaviour, was removed on 20 August 2026: 48 files, 56,072 lines. This changes more than a file count. Everything the witness used to compute and that the port to flang has not caught up with is today computed by nobody — and the tree says so plainly instead of keeping quiet: the probes written against the witness lie in flang/test/ and do not run, because each one breaks on importing a removed file.

The self-applying lexer is completely total — 99 functions out of 99 — and this is worth noting, because before there were 54 out of 88. The difference is exactly one: the character-by-character traversal has stopped iterating over the position. The difference “size minus position” was decreasing, that is, a number with no constant step; now the string is broken down into a list, and the recursion over the tail is proven.

The bootstrap circle is closed by a seed: the tree holds the same compiler, printed in advance into C99. A single make builds the binary out of the seed, that binary prints the sources anew, a second binary is built from that printing — and the second one must match the first byte for byte. This is checked by sh scripts/raskrutka.sh --check over seven files, and a divergence is named by file, byte and line rather than by the words “did not match”. The seed is reprinted by hand, and until it has caught up with the sources the circle stays open: the check refuses and says on what.

Installation and Portability

The release includes a compiler, already written in C99, so installation requires only a C compiler:

brew install digitable-lol/tap/flang

The formula puts down one binary flang, a library with headers, the C runtime sources in share/flang/c and the manual page man flang. From the outside it needs only make; Node.js is required neither for installation nor at work. This distribution method has also been used by other self-hosting languages: Go used to ship generated C code for a long time, and Nim still does. The initial bootstrap problem remains for those who develop the language itself.

The second path is to build from source; it is also the path for whoever edits the language itself:

git clone https://github.com/digitable-lol/flang.git
cd flang
make -C bootstrap -j8

What comes out, bootstrap/flang, is the same tool the formula puts down. Node takes no part in the build.

What got installed is asked of the binary itself: flang --version and flang -v answer flang 0.7.3, flang --help and flang -h list the commands, and man flang describes them in detail.

The check lives right in this binary: flang check файл.flang performs the walkthrough, linking, type checking, termination, proofs and examples, and prints comments in words — with code and location. On a file that passes, the answer carries the word “проверено”; a file with a type error takes the binary out with exit code 1 and names the code of the trouble — FLANG_TYPE. The proof ledger is printed by flang check --proof: for a machine --json, into a file --записать.

The binary has twelve commands — check, test, run, emit, ast, tokens, facts, io, lock, package, repl and lsp. The binary also computes on its own: flang run файл.flang --function «Имя» evaluates a function without Node and without cc. And it prints into all nine targets: flang emit файл.flang --target c and the same for go, rust, java, js, elixir, python, csharp; the directory given by --out is created on its own.

The service for an AI assistant lives in the same binary, but it is offered not as a subcommand: it is a key, flang --mcp-mode — JSON-RPC over the standard streams, one message per line, and it is the assistant that starts it, not a human. It gives two tools: flang_check checks a whole program together with the ledger, flang_prove answers what one named promise is proven by. There is deliberately no “ok” field in the answers: the three verdicts travel separately — “proven” about all inputs, “grid N” on the author’s values, and “declared, not proven”. How to wire the service into an assistant is printed by flang --mcp-mode --help.

One caveat about printing has to be known in advance, or it meets you on the very first command. The target’s runtime travels into the output verbatim, that is, it is read from disk — looked for in --runtime, then in $FLANG_RUNTIME_DIR, then next to the installed binary, in share/flang/<цель>. The formula puts down one runtime out of eight — share/flang/c — and the release archive carries only that one. So printing into C works straight out of a brew installation, while for the other seven targets --runtime has to be pointed at a source tree (flang/src/emit/<цель>).

The shell flang repl does not call the evaluator yet: it prints the session in C, compiles it with the system cc against the runtime installed next to it, and runs it; without cc it does not switch off but continues to check the walkthrough, types, and termination.

The runtime does not contain architecture-dependent constructs; alignment is calculated by combining basic types, meaning the maximum value for the platform is taken. The compiler was built using a cross-compiler for RISC-V and run under emulation without a single change to the source code: the values matched x86-64 to the last digit, including 0.1 плюс 0.2 = 0.30000000000000004, NaN, and Infinity.

Limitations

First-class functions exist and are printed for all eight purposes. The restriction has been lifted by defunctionalization: a value-function is a tag, application is a dispatcher over the final list of tags. Therefore, purposes without closures are not affected, and the provability of termination is also preserved: the list of tags is finite, the program is visible as a whole, and the termination analysis has not changed by a single line—it has only changed in what it consumes.

Printing reduces the program in a SINGLE pass before the backends: the tag becomes a variant, the application becomes a dispatcher call, and none of the eight higher-order backends see it at all. In a program without value functions, the pass returns the same object, so printing the rest cannot change by design—this has been verified byte-by-byte on all programs in the repository.

One discrepancy is identified and left as is: a tag that the program does not generate can be provided externally, and both sides reject it, but with different codes—the calculator with its own, the printed walkthrough with its own. To reconcile them would mean introducing a built-in form of “trigger an error with this text” and modifying eight runtimes, which is exactly what the pass and the code are written to avoid. There is no discrepancy in the meaning that the program can construct itself.

Parametric polymorphism also works in the repository. Type parameters are declared for types and functions, applied, and inferred during the call, and printing them does not cost anything — all eight goals erase types anyway. For a long time, it was impossible to use this: the parser did not understand self-application of polymorphism, and the verification corpus is assembled according to the directory mask, so the first such file in the library would break the fixed point. Now it understands — and the monad can be expressed: тип «Возможно» от «А», функция «Обернуть» от «А», binding to a type parameter функция из «А» в («Возможно» от «Б») pass the walkthrough, types and completion. The library has been moved onto it: flang/stdlib/optional.flang is the optional type over a type parameter, flang/stdlib/result.flang is the result type over a value and a failure, and flang/stdlib/higher-order.flang went the same way, where four functions with pairwise identical bodies became two without losing a single example.

User-defined properties are checked, not proven. What is proven is termination, types, and whatever the proof kernel accepts: it has zero axioms, every step must name a fact, and the kernel only checks—it cannot search and must not. User-defined properties and examples are checked on a finite grid of inputs. The ledger of this is printed by flang check --proof, and its words are not interchangeable: “proven” stands only at statements about all inputs, while at a grid it says “no violations found”, because “we did not find” and “there are none” are different statements; and where the examples were not run at all, it says “violations were NOT LOOKED FOR”, which is a third thing and reduces to neither of the first two. The laws of the categorical surface are computed by nobody today: the layers exist but are not wired into the binary. The documentation must distinguish between these cases: “checked on N inputs” is not the same as “proven”.

Extending provability is possible: conditions that fit into linear arithmetic are solvable, and connecting a solver to verification conditions remains an open problem.

Effects are expressed through description, not execution. The language is pure; working with the network or files involves constructing a description of the action that is executed by the host, the environment in which the module is printed. The operations are declared by the language itself as a single closed sum «Поручение» — not by the author of a program, because an operation is a contract between the language and the host; the set covers files and the octets in them, directories, launching processes, connections, network requests, time and random numbers. Next to it stand the declaration план and the command flang io with four exit codes: 0 — we got there, 1 — the program gave up on its own, 2 — a malformed call, 3 — the tool broke. The host here is its own, not one on Node, and its boundaries are named by refusal rather than by silence: there is no screen (FLANG_IO_NO_SCREEN), there is not a byte of its own cryptography, and https is carried out by an external curl — with none on the machine the answer is FLANG_IO_NO_TLS. Functions that construct operations are checked with ordinary examples and remain total—the network is not part of the language. There is no input-output monad, and in its place there is a continuation machine (flang/cat/SPEC.md, “Why isn’t this a monad?”). The execution layer for a PRINTED program, however, is made for one target out of eight — Node.

fspec: a proven rule and what keeps it from being cancelled

The mechanism is called fspec, and it rests on one thing: a spec is not markdown but a program in the language itself. A domain rule is written next to the function, and the compiler proves it for all inputs, not for those that will arrive in production:

модуль «Спека 1: потолок скидки»

тотальная функция «Потолок скидки»
  принимает сумма: число
  возвращает число
  обеспечивает «скидка не больше 30» результат не больше 30
  пример «потолок»
    дано сумма равно 1000
    ожидается 30
  30

There are four parts, and each does work. обеспечивает «имя» <цель> is the rule itself, what holds about the result; it is carried by the proof kernel at every check. требует «имя» <условие> is when the rule applies; that is the caller’s duty, and conditions that cannot hold together break the very first call. пример … ожидается … is a sample from life, run at every check rather than on demand. использует «Спека N» из "./…" is the link to a spec written earlier: the inclusion pulls in its functions, and the successor’s report contains the statements of both.

The last line is what the whole thing was built for. The rule “the discount is no more than 30” is written once; a month later a requirement arrives, “a promo order gets a bigger discount”, someone writes a second function and a second spec — and whether the first rule is still true is answered not by two people proofreading, but by a run:

make -C bootstrap -j8                  # собрать компилятор, если его ещё нет
bootstrap/flang io fspec/guard.flang   # или короче: ./ярлык spec:check

The answer is a single line with numbers:

спеки согласны: спек 42, утверждений 295, и каждое доказано из нуля аксиом; обещаний в слепке 100, и у каждого цель та же; видов перевода 2, и каждый обещает то же, что основной

A spec is accepted only if every statement of its own is proven and every statement of its predecessor has stayed proven in the successor’s report. A statement is identified by the pair “function plus name”, so a renamed or cancelled rule stops being confirmed and that is visible from a run. Exit code 0 means “accepted”, 1 means trouble, named by file, function and the name of the statement. The argument behind such an acceptance rule is direct: the language has zero axioms, and therefore no falsehood can be derived from a set of proven statements — there is nothing to derive it from.

What’s new

New here1

Easier now3

flang — language description