Releases

A release is a vX.Y.Z tag, and behind it an archive and a package publication. This page is printed from the tags: as many entries as there are tags, and a release cannot be skipped.

There are three boxes: what appeared, what changed, what broke. An empty box is not printed — "broke: nothing" nine releases in a row tells the reader nothing.

The entries below are about the language, not about the work on it. What has landed on the trunk since the last release is shown by the merge journal (in Russian); every commit subject is in the commit journal.

0.7.29 — 18 October 2026

Prebuilt binaries and a one-command install, category laws are proved

What appeared

• Prebuilt binaries for Linux and macOS, installed with one command. No C compiler and no sudo: curl -fsSL https://raw.githubusercontent.com/digitable-lol/flang/main/install.sh | sh puts flang into ~/.local/bin and checks the archive against the release SHA256SUMS. Other ways: brew install digitable-lol/tap/flang-package, asdf, deb and rpm packages.
• A playground in the browser. On https://digitable-lol.github.io/flang/en/playground.html a program or a syllogism is checked right in the tab: the compiler is built to WebAssembly, nothing to install.
• An installed flang finds the standard library. использует «Lists» только «Длина» (uses Lists, only Length) works in a program in any directory: the library sits in share/flang/stdlib next to the binary. Before, this worked only inside a clone of the repository.
• The kernel proves the laws of a monoid, functor, isomorphism and natural transformation — for all values, not on a grid. check --proof prints them in a section of their own, for example on flang/ct/yoneda-preorder.flang: законов утверждениями 9: доказано ядром 9, не доказано 0 (laws as statements 9: proved by the kernel 9, not proved 0); in --json it is the lawClaims field. A law that is not proved is named. Monad laws are still computed on a grid.
• flang test runs прогон (run) blocks and checks their expectations. Each block counts as an example: a wrong expectation is exit code 1 and the message у процесса «Счётчик» состояние {"всего":5}, а ожидалось {"всего":999} (process Counter has state 5, expected 999).
• check --proof prints the proof steps for most statements: which field or which call was unfolded and on which source line, for example ход 1 поля ⟨«Пополнить» от ( счёт ) и сумма⟩ строка 15 … (step 1, fields, line 15). Some statements still show only the rule name.
• always properties of processes are checked by exploring a finite model. A model is processes, their states and rules "on this letter, move to that state and send these letters"; the exploration walks every order up to a given depth. The answer is either the shortest counterexample run or "not violated … this is not a proof". For the model flang/concurrency/temporal/models/deadlock.flang the answer is НАРУШЕНО, встречный прогон, шагов 6 (violated, counterexample of 6 steps). Both proof checkers (in C and in Lean 4) replay such records on their own: ПЕРЕБОР СВЕРЕН: встречный прогон переигран, шагов 6, в конце свойство «без тупика» ложно.
• The printed C is checked against a reference. flang run-script translation:validate prints examples to C, builds them and compares the answers of the programs with the answers of a reference semantics in Lean 4: СООТВЕТСТВИЕ ПРОВЕРЕНО для 146 функций, вне валидации 4 … расхождений 0 (146 functions agree, 0 differences). It rejects six deliberately broken versions of the printed C.
• A grammar of Russian sentences on typed words. flang run flang/ct/russian/parse.flang --function «Разобрать» --args '{"предложение":"мама читает книгу"}' answers грамматично: … связи: мама—читает, читает—книгу (grammatical, with the links), and for «мама читает книга» it answers не грамматично: неверный падеж (wrong case).
• Unicode 17 in the standard library: normalization (NFC, NFD), grapheme clusters, case-insensitive comparison and explicit decoding of bytes. «Графемы» от "👨‍👩‍👧🇷🇺" gives two graphemes; «Равны без учёта регистра» от "STRASSE" и "straße" gives да (true); «Раскодировать байты» от "UTF-8" и [104, 255] gives a refusal at position 2 with the reason «байт не может начинать знак UTF-8» (this byte cannot start a UTF-8 character).
• In the flang repl shell you can write statements, theorems and syllogisms. The shell answers at once: утверждение «сложение перестановочно»: доказано (код 0) (proved), refuted with a counterexample, or not proved with the reason.
• A reference semantics of the language core is written in Lean 4, and for every step the independent proof checker replays there is a Lean proof that the step is sound.

What changed

• An exported function may call a hidden helper of its own module. A program that imported such a module used to fail check; now it passes, and calling the hidden function directly is a FLANG_UNKNOWN_NAME error that says the module declares it but does not export it.
• A nested object is a clear error instead of a crash. The line вложен объект (nested object) gives FLANG_PARSE … старое слово (an old word): declare the nested record as an object of its own and refer to it by a field.
• Linking errors name the file, not only the line and column.
• make install from a clone of the repository does not install the standard library yet, so a program with использует «Lists» outside the clone will not find it. Install flang with install.sh, brew, asdf, deb or rpm instead: those carry the library.

What broke

• run on a program that does not pass checking exits with code 1, not 3. The same with --на-веру (on trust): consent to unproved code does not lift parse, link and type errors. If a script waited for code 3, test for a non-zero code or fix the error the message names.
• A name missing from an только (only) list is now a FLANG_UNKNOWN_NAME error, whatever the order of the использует (uses) lines. Before, it sometimes passed when another file imported the same module more widely. Add the name to the только list or remove the call.
• check --proof exits with code 3 when some statements rest only on examples or on a grid of values. Before, this was code 0 with the words "verified with a support". For example, flang/stdlib/lists.flang (42 proved, 24 on the grid) now answers НЕ ДОКАЗАНО — ОПОРА НЕ СУДИЛАСЬ (not proved, the support was not judged) with code 3. If your build treated only 0 as success, prove the remaining statements or accept 3 as "not everything was checked".

0.7.28 — 14 October 2026

Examples inside laws run, mistakes in categories are caught at compile time

What appeared

• flang test and flang check run the examples inside a закон (law) block. These examples never ran before, so a wrong expectation passed silently. Now a wrong expectation is exit code 1, and the message names the law, the example, the expected and the actual value: ожидалось {"номер":777}, получено {"номер":500}.
• check verifies how a category is put together. An arrow that was never declared, an arrow listed twice, a composition through an arrow outside the category, arrow ends that do not meet are now errors with exit code 1 and a line number. For example: FLANG_CATEGORY_UNKNOWN_ARROW в файле warehouse.flang, строка 9, столбец 1: категория «Склад»: стрелки «потерять» не объявлено.
• check --proof says why an equality over a long chain of calls was not proved. Substituting proved properties of functions takes at most 64 steps. When that is not enough, the statement stays unproved and the answer says so: переписка доказанными равенствами исчерпала «Предел переписки» — 64 шага (rewriting ran out of its 64-step limit). Before, you only got "declared, not proved" with no reason.
• Both proof checkers (in C and in Lean 4) re-check statements with a quantifier inside и притом (and) and если (if). The kernel proved such statements before; now their proofs are re-checked independently.

What changed

• A file with categories whose laws were all checked passes check with exit code 0. Before, every such file got code 2 with a note that category structure is not checked. Of the 25 examples in flang/ct, 16 now pass with code 0, up from 7. The other 9 get code 2 and name the law that could not be checked.
• check --proof over the standard library is a little faster. The kernel takes proved properties only from the functions that appear in the statement being proved. Over the 55 files of flang/stdlib the total time is 5773 s on 0.7.27 and 5518 s now, 4 % less, with the same results.

What broke

• A wrong example in a закон block now fails test and check with exit code 1. Fix the expected value in the example or the function itself; the message names both values.
• A mistake in how a category is built is now exit code 1 from check, not 2. Declare the missing arrow with морфизм or drop it from the категория block; delete a repeated line.

0.7.27 — 14 October 2026

Grown-up proofs: algebra, terminating recursion, LaTeX formulas; HTTPS without curl

What appeared

• The kernel proves algebraic identities over integers. check --proof expands both sides of an equality into a polynomial and compares them, like Lean's ring. For example, (a + b)·(a + b) = a·a + a·b + b·a + b·b is proved for all exact integers a and b. Over число (double) these laws are false, so you get a refusal that says why.
• Proofs are re-checked by two independent programs, one in C and one in Lean 4. The kernel writes the proof to a file, and each checker replays it on its own. A kernel bug or a forged record gets caught; whatever could not be replayed, check --proof names. Both checks run in CI on every push.
• The compiler proves that recursion terminates. Write убывает н (decreases n) on a function, and check either proves that н shrinks on every call or refuses with FLANG_NOT_TOTAL. н минус 1 over non-negative numbers is proved; a 3·н + 1 step (Collatz) is rejected at compile time, before anything runs.
• A proved property of a function is used in other proofs. Once f(x) is proved equal to some expression, the kernel substitutes that expression wherever f is called, like simp. A chain of 18 nested calls is proved.
• Write formulas as in a textbook. formula:read '∀ a ∈ ℤ, ∀ b ∈ ℤ, a + b = b + a', or the same formula in LaTeX, becomes a flang statement that the kernel checks right away. It also works the other way: formula:print file.flang prints a file's statements as formulas and as LaTeX. ℕ means exact integers, ℤ means 53-bit integers (the translator warns you), ℚ≥0 means exact fractions. ℝ and ℂ are not supported, because double does not obey the field laws.
• A long expression can wrap onto the next line inside parentheses. The continuation indent does not matter, and errors point at the real line and column.
• Monoid, functor, monad and isomorphism laws are checked at compile time. The compiler tries a set of values and looks for a counterexample. A broken law is exit code 1, an unchecked one is code 2. This is testing, not proof, and the compiler says so. flang/ct gains eight category theory examples: product, coproduct, pullback, an adjunction, the Yoneda lemma on a preorder, a monoidal category, Maybe as a monoid, Kleisli arrows.
• HTTPS works without curl. A TLS 1.3 client written in flang is built into the binary. Root certificates come from the system or from --trust-roots file.pem. UDP send and receive were added.
• Scripts (.fscript) compile to C, Go, Rust and Python. flang_cli --plan <name> runs a plan in the chosen language. Files, directories, environment variables and arguments work; other operations answer FLANG_IO_NOT_WIRED for now.
• Compiler messages in English. Set FLANG_LANG=en or language = en in .flangrc. Translations live in a plain table, flang/messages/catalog.tsv.
• Generated code checks types at its input. In all ten target languages the program rejects input that does not match the declared type, such as a negative number where неотрицательное (non-negative) is declared.

What changed

• A module linking error names the file: the message starts with в файле <path>:.

What broke

• HTTPS no longer calls curl. A binary built without the embedded TLS client (including flang emit --repl) answers an https request with FLANG_IO_NO_TLS. Certificate checking cannot be turned off.
• A function with убывает whose measure does not shrink now fails check (FLANG_NOT_TOTAL, code 1). Before, it only failed at run time.
• An import name clash is now an error. This is the case where an imported function calls a hidden helper of its own module and another file has a helper of the same name. The error is FLANG_DUPLICATE_NAME. Fix it by listing the helper in только or renaming it.
• A wrong monoid, monad or functor law is now exit code 1 from check. These laws were not checked before.
• Badly typed input to a generated program is now FLANG_TYPE in every target language.

0.7.26 — 11 October 2026

TLS in the language, host entropy, cost before the run, a kernel cache and a second checker in Lean

What appeared

• TLS 1.3 is assembled in the language and runs printed (ADR-0078). flang/stdlib/tls-client.flang and certificate-path.flang: the handshake, the server signature RSA-PSS (all 60 vectors of pss-vect.txt accepted, forgeries refused), the chain to a root, the validity window, basicConstraints and the host name, against the live host www.google.com up to GTS Root R1. The «Запросить» order over https still goes through curl: named, not hidden.
• The host hands out octets from the system random source (ADR-0077): the order «Случайные октеты» with a сколько field answers «Октеты». The main argument of ADR-0007, that a program has nowhere to take a secret from, is gone.
• Exact integers and exact fractions print into all ten targets; every target runtime computes them itself; целая часть is a built-in unary form (ADR-0074); the remainder over the exact integer; probes compare the evaluator with the ten targets byte for byte.
• The cost of a function is known before the run (ADR-0083): flang run --cost and the runner's cost field print the step and memory bound from the input sizes.
• A proof cache remembers kernel answers across runs in a signed directory (ADR-0080); the one-run memo of ADR-0051 became memory between runs.
• The second record checker is written in Lean 4 (ADR-0076) and crosschecked with the C checker; only what the checker replays counts as proved (ADR-0073); check --proof says how much was replayed.
• Kernel rules: segment induction, integer tightening and enumeration of a finite sum (ADR-0075: Инд5, Инд6, Цел3) and rewriting a goal by a proved equality with a quantifier inside a formula (ADR-0084: Переп1, Скл1–Скл3, Св2), each with a Lean lemma and a trap.
• Normal parallelism (ADR-0072): the pool, the pure map and a proved monoid; printed C, Go, Java, C# and Elixir map and fold a list in chunks; the kernel judges monoid laws and marks the folds it cuts.
• A foreign language enters through an untrusted translator (ADR-0058): C loops, assignments, calls and structs are translated to flang and judged by the kernel.
• Printed code follows the canon of its target (ADR-0081): the formatter and the linter of each of the ten targets accept the print without edits; C and C++ are laid out like clang-format LLVM, C# like dotnet format.
• DESCRIPTION.md mirrors the language: it names every lexer word, every flang --help command and every settings key, a census guard keeps it so, and the release body lists the changed sections of the description.
• The checker's case split reads more bodies and links atoms: требует hypotheses and replayed callee promises are facts, lengths are counted and split by the half; the user program greeting is now replayed by the checker.

What changed

• The licence lives in one LICENSE file: SPDX lines left the sources (112 files), the licence guard checks one root file.
• The seed was reprinted twice by the batch after 0.7.26: a print by its own printer and a second print that is the fixed point (compiler_flang.c 43 917 383 bytes).
• The site number guard measures what numbers:build prints; the corpus numbers on the site were retaken on the current tree.
• The package lock: every form of a dependency reaches the lock file; registry resolution is proved by a corpus and a forgery.
• check messages name the proof report in plain words; the registry page is printed without internal words.
• Census guards are flang plans proved by the kernel, not shell: the hand-written list census, the judge census, the uncalled-check census.

What broke

• A record with nothing proved answers 3, not 0: the checker no longer stays silent on an empty record.
• The second checker module and the hand-written-list forgery code are English words; the old names are not read.
• The kernel refuses induction when a pattern name shadows a parameter: programs that lived on that hole stop proving.

0.7.25 — 6 October 2026

Exact integer and exact fraction, a child's limit named by the order, the registry page

What appeared

• The exact integer is a type of its own, not a new name for number (ADR-0036; tasks 1908, 1412, 1413). exact integer adds, subtracts, multiplies and compares without the 2^53 ceiling; a value is a list of base-2^22 digits without sign, the canon (no leading zeros) holds at every action, a non-canonical literal is refused by the typechecker. Digit addition is printed into all ten targets. The associativity of its addition is proved by a kernel rule, the first ring rule with a Lean lemma and forgery probes.
• The exact fraction (ADR-0062; task 5243). A pair of exact integers, numerator over denominator, reduced at every action; plus, minus, times, divided by and the order by cross multiplication; a written literal is checked for canon (a pair, canonical halves, non-empty denominator, reduced); below zero and division by the zero fraction are FLANG_PROPERTY refusals by word; it does not mix with number or exact integer. Probe set exact-fraction: 26 of 26; the previous seed refuses all 26.
• The remainder over exact integers (остаток от; task 5245): the glibc generator step is exact where double rounds the product 1103515245*8388607.
• A child's limit is named by the order, not by the host (ADR-0061): the order 'run a process with a limit' (memory in KiB, time in ms) and the reply 'process cut off', which carries what was printed before the cut. Two benches, the memory limit and the node death, move from shell to plans.
• The package registry page is printed from the ledger and published on Pages (ADR-0059): the registry is a ledger of names, not a store of code.
• check asks the plan judge: twelve forged plans that used to pass are refused.
• The experimental directory flang/experimental/: Russian morphology for syllogisms and a demo that fills the dictionary and judges a text.
• Every checker move has a Lean theorem or a debt row (ADR-0064; task 4791). The list of шаг_вывода moves is taken from checker.c by an instrument, not written in prose: 83 moves, 78 in the Lean acceptance, five stand as debt rows with a task number. Н6 and О9, nine days without a theorem, enter the acceptance; the lean-rules:check guard runs on every push, goes red both ways, and its three forgeries run in CI. A hole closed on the way: a case split accepted a false postcondition by pasting the condition as text under a binder; the checker now refuses.

What changed

• The printed Makefile names each object's headers (task 7182): editing a .h rebuilds the dependent objects; it reached the seed only on the second print in a row, because the Makefile is printed by the printer, not by the sources.
• The seed was reprinted five times in two days, one print on gpu costs 79-83 minutes (five rows added to docs/reprint-ledger.tsv); the print fingerprint names the commit the seed came from.
• The 'limit for a foreign process' decision is ADR-0061 — number 0056 on the trunk was already taken by the quantifier measurements; seven references moved.
• 122 added lines longer than 120 characters were shortened without bypassing the growth guard: parser lists broken after commas, lexer table pieces split, bench and guard examples moved to twin functions that render the answer as a list; example values are measured, not predicted.
• The C-2 report of the rule-ledger guard names the rule count on one line and the per-ADR breakdown on the next; the C-6 line about the checker.c budget is seven words shorter.
• The roadmap page is a dated plan to 1.0. A month-by-month table from October 2026 to April 2027, milestones 0.7.25, 0.8, 0.9 and 1.0, seven conditions for 1.0 and what is ruled out; the undated text is gone.
• ADR-0067 on binary releases is proposed, no code. A release will ship binaries for four triples with one SHA256SUMS; five tasks (7959, 8128, 1710, 1504, 1098) and five decisions await the owner. The names of the decision that no source knows stand in the register of names declared and not made.

What broke

• The division refusal over two exact integers now lists four actions, not three: plus, minus, times and remainder. Probes expecting the old word are re-taken.
• The fraction enters none of the ten print targets — the emitters do not know it; a program with exact fraction runs only in the interpreter. There is no keyword for the integer part of a fraction; docs/flang/SPEC.md and DESCRIPTION.md describe neither exact type — the debt is named in ADR-0062 §6.

0.7.24 — 3 October 2026

A linter in the language, a kernel memo, and three closed soundness holes

What appeared

• flang lint — line length and conditional depth, limits read from .flangrc. The keys are max-line-length and max-conditional-depth, and lint (refuse) says what to do about a violation. The pre-push gate judges your change only: an added line must fit the limit, a touched function must not be deeper. The tree does not meet the limits and no debt ledger is kept — that is the decision of ADR-0053: flang lint over the tree finds 32342 lines longer than 120 characters and 1365 functions nested deeper than 2, across 703 of 1301 files (measured 3 October 2026). This release's own change took 77 long lines out of the lines it touched and left the rest of the debt where it was.
• Short commands live in the settings file. flang run-script <name> takes its line from .flangrc; shortcuts no longer hide in a separate script, and flang run-script with no name prints the ones there are.
• A library profile in .flangrc. A program sees the standard-library modules the profile names: a smaller closure and no name clashes.
• A kernel memo: within one run a pure call is computed once. It speeds up proof checking and the seed print; in the printed C the memo is a wrapper around three kernel functions.
• The block literal """ strips the common indentation of its continuation lines (ADR-0052). Long text no longer has to start at column zero, and a long line in code is no longer a choice between the line limit and the truth.
• The library gained long division with remainder, gcd and exact rationals. The division and the gcd live in bignum.flang -- at 0.7.23 it had neither; its obligations are still 9, the new functions carry no postconditions. rationals.flang is a new file: fractions over long integers, 17 functions and 13 obligations (reduction, the four operations, comparison, a harmonic sum). fmath.flang is new as well, but it holds no functions -- four standalone statements about the length and the sum being non-negative, and nothing in the tree cites them yet.
• Reasoning in sentences: a proof is written as sentences, premises as assumptions (ADR-0050). A step names the kernel rule, not a line number.
• A guard for forgotten temporaries of checks. An untracked .flang-storozh-* directory, or a file with "probe" in its name, left in the tree after a killed run is reported with its path and exit code 1; the six places where a temporary has to live in the tree (the compiler resolves imported modules relative to the file) are named by the guard itself, with the reason.
• The decision about exact integers is written down, and their absence is held by a probe (ADR-0036, task 1908). Numbers in the language are still IEEE-754 doubles, and integers are exact up to 2^53-1. The set flang/proof/probes/exact-integer/ shows on every CI run that there is no exact integer in the language: the literal 42 stays a number and the kernel has no ring rules for it. The probe will turn red on the day one appears, and that is its job.

What changed

• The independent checker replays more. By-assumption steps from the statement's premises, property steps, citations across files, field projections, module types and dependency sets as the linker sees them, and what the kernel proves in your programs, not only in the language's own tree.
• An identity over an open term is no longer called a lie (4850). The move "substitute a term for itself" is accepted without evaluating anything, and a term that cannot be evaluated is reported as a place the run did not undertake (code 3) instead of a disagreement (code 1): a place the run did not check is not a lie.
• The independent checker has a strict key. It asks something else than the default: not "does the record contradict the source" but "is it proved at all". At least one obligation is required and every one of them must count as proved, otherwise the outcome is 3 with the reason named. On the nine programs of the strict probe set six answers of zero turned into three - the record for a program with a false postcondition among them, the one all three instruments used to accept with zero.
• A proof record that lags behind its source is refused, and the checker rebuilds itself when its source is newer than its binary: an old binary no longer judges new source silently.
• The tree's verdict is PROVABLE, and the probe suite under it has grown. The share replayed by the independent checker stands at 100.00 % — 650 obligations out of 650; the verdict's threshold is exactly 100 %, and the share meets it. Against 0.7.23 it is not the share that grew but the suite that holds it up: forgeries in the manifest 36 -> 38, forgery probes 575 -> 631, honest probes 274 -> 315, unreachable places carried out 27 -> 30, and the ratchet was raised with them. The verdict's four checks: the calculator is out of the checking program, the share is at or above the threshold, the probe suite passes, and the suite has not weakened. Measured by io scripts/provability.fscript --plan Verdict: for 0.7.23 the CI run of 29 September 2026 on main, for 0.7.24 the run of 3 October 2026 on the release branch.
• The tooling moved off shell and Python onto flang plans. Guards, probes and counting instruments are plans now; the pre-push gate refuses growth of shell, Python and stray markdown, and CI judges the commit message against the convention (prefix, subject length, ASCII only).
• The guide and the site are written in plain words. The README says what the language does and how to install it; docs/DESCRIPTION.md is no longer pinned to a release (the line "this description matches 0.7.23" is gone) and no longer prints numbers that change from build to build. No dated reports are left in the tree except two under docs/archive/, which the ROADMAP cites; 418 files left docs/ over this release.
• A date from a day count is right below year one. A correction written for truncation fired a second time under floor division, and day -719834 gave -719833. The round trip days -> date -> days now agrees on 1038 consecutive days at the era boundary, on 7240 days with step 1009 and on 4000 pseudorandom ones - zero disagreements.
• The seed fingerprint finds its own commit by content. It used to name a sha that died in a rebase, and the fast check refused with "the commit is unknown to the tree": four of five values over two days were dead. On the red path the instrument now looks for the youngest commit whose print inputs match the fingerprint file for file, and the --perekommit key rewrites that one line.
• The flangtutor guide accepts correct answers. A lesson's value is read from stdout alone, not together with the error stream that carries the proof verdict; the guide's list of language words caught up with the lexer table (649 phrases against 647), and the guide's probe is green as a whole.
• Five Cyrillic paths in the tree instead of 67 (four instead of 66 outside flang/proof). What is left is named in the ledger with a reason: four files in flang/test are named by flang/self itself and travel into the seed verbatim, and letters.фп is an extension fixture. The transliterated names in flang/self are gone as well: five files (zapis.flang -> proof-record.flang and four more) now carry English names. The guard answers "5 paths, all in the ledger — none new", exit 0.
• The growth gates judge the change, not the state of the tree. A rename no longer looks like a new file to them: git --numstat reports a fused path docs/{old => new}, and the gates resolve it to the new path. The similarity threshold is 50 % (an amendment to ADR-0053).
• The Cyrillic-name guard looks at the whole path, not the last segment. A Latin file name inside a Cyrillic directory used to pass in silence; the verdict now names the full path.
• flangtutor picks its locale and its awk by a run. On a machine where /usr/bin/awk is mawk the lesson arrived as garbage: mawk cuts the closing guillemet by byte. The pair (locale, awk) is now checked for keeping UTF-8 whole, and if no pair qualifies, painting is dropped and the text stays whole.
• The gates stopped lying by silence. The pre-push gate killed a check that stayed silent longer than 200 s and answered "checks not run": on this release's range not one of its 21 checks ran (lint:growth is silent for about 290 s). The silence budget is 900 s now. The line-length gate itself asked git for the whole diff and hit the 1 MiB output cap on a printed seed of 685001 lines -- it now asks only for the five extensions the linter reads, and that is held by a negative control: without the :(top) prefix the pathspec matches nothing and the gate would have gone quietly green.

What broke

• A theorem whose hypotheses the statement lacks is refused (5311). Such a theorem used to prove a statement weaker than the one declared; programs where that passed will now be red, and rightly so.
• Totality sees calls made through function values (3870). A function that counted as total only because the call went through a value no longer counts as total.
• A postcondition restricted by таких что is cited only once the restriction is discharged (4573): citing it earlier is no longer accepted.
• Three refusal codes and the note index got English names. If you matched the old code strings, fix the match.
• The shell and Python instruments are gone (scripts/target-census.sh, the Python instruments of the proved share). Flang plans count the same things; the old call paths no longer work.
• A push stops at the linter when an added line is longer than the limit or a touched function is deeper: the limits come from the tree's .flangrc, not from habit.
• flang test exits 3 when the scenario blocks have not been run. A file with прогон blocks used to exit 0 and say "2 examples, 2 passed", so a deliberately false expectation inside a block passed in silence. Next to the example count there is now a line "scenario blocks N, run 0", and the outcome is "done, but not everything was checked". A build script that read the zero will turn red, and rightly so: the blocks are still not executed (the scheduler is outside the binary's closure, task 1104).
• 153 shortcuts live in .flangrc and carry English names. At 0.7.23 the settings file held none. Whoever called the old Russian names now calls the English ones: подсчёты:проверка → counts:check, тесты → tests, столкновения:проверка → link-collisions:check.

0.7.23 — 29 September 2026

Record fields are checked against their type, and runs have a memory limit

What appeared

• --memory-limit N (--предел-памяти) — memory cap for a run. Works with any command. check, test and run default to three quarters of the machine's memory; 0 removes the cap. At the cap the run stops with exit code 5 and names the function being evaluated.

$ flang run runaway.flang --function «Раздуть» --args '{"текст":"а","раз":28}' --trust --memory-limit 32M
FLANG_MEMORY: прогон остановлен на пределе памяти 32 МиБ: занято 25 МиБ, просили ещё 25 165 880 байт
  считалась функция «Раздуть», шагов программы 544
                                                                    exit 5

Issue #160.

• Every proof step names its kernel rule. A step line in a --record file ends with правило «…»; --proof --json has a stepRules field. The independent proof checker compares the name with the rule it applies itself.

What changed

• A record field is checked against its declared type. A неотрицательное (non-negative) field accepted -7, and the kernel proved a postcondition that the run then violated. Such a program now fails type checking with FLANG_TYPE … поле «шаг» записи «Мера»: ожидался неотрицательное, получен целое, exit 1.
• flang io: a process that outlives the host timeout is a FLANG_IO_TIMEOUT failure. It used to be reported as «Процесс убит» SIG9, as if killed from outside. --timeout is a silence timeout counted from the last output byte, 30000 ms by default, and is now in flang io --help. Issue #162.
• The interpreter frees memory on deep recursion. Beyond about 500 nested calls memory was never reclaimed and grew with every step. «Числа до» от 1000 used to hit 3.6 GB and now runs in 370 MB. Issue #160.
• разделить … по (split) and содержит (contains) in the C runtime find the separator with memchr. On 100 MB of text: split 0.47 → 0.08 s, contains 0.39 → 0.008 s; step counts are unchanged. Issue #161.
• .flangrc keys are English: language, surface, color, page, version, name, license, repository, issues, unproven. Old keys are still read and name their replacement.
• String literals are printed verbatim in proof records. Spaces used to be inserted inside strings: " : //" instead of "://".

What broke

• Module search by name stops at the project root — the nearest directory with .flangrc, .git or flang.package. A file above the root no longer replaces a project or library module, and a module that lives only there is not found (FLANG_IMPORT_NOT_FOUND).

Migration: move the module into the project, import it by path (использует «Мера» из "../mera.flang"), or set FLANG_MODULE_ROOT.

0.7.22 — 26 September 2026

The следует syllogism and correct code points outside the BMP

What appeared

• следует (follows) — derive a statement from premises named above it. The conclusion is a separate block that cites a proved statement with по свойству.

утверждение «все люди смертны»
  для всех кто: «Человек»
  утверждаем («Смертен» от кто)

следует «Сократ смертен»
  дано сократ: «Человек»
  утверждаем («Смертен» от сократ)
  по свойству «все люди смертны»

$ flang check socrates.flang --proof
утверждение «Сократ смертен» — доказано: терм принят ядром, 1 шаг, основания: утверждение «все люди смертны» — утверждение обо ВСЕХ входах

Without the по свойству line the conclusion is not proved:

FLANG_PROOF_STEP: теорема «Сократ смертен»: ни одного шага        exit 1

What changed

• код символа (character code) in the shell: characters outside the BMP. flang repl returned 240 — the first UTF-8 octet — for any such character, while flang run answered correctly. Both now agree.

$ flang repl
» код символа "𝒜"
119964
» код символа "👍"
128077

Issue #103.

• The binary itself has no --step-limit key. An earlier edition of these notes said the key works with any command. In 0.7.22 only flang check parses it.

$ flang --step-limit 100000000 emit file.flang --target c
flang: неизвестная команда «--step-limit»              exit 2

What broke

• The seed print scripts are renamed. This affects those who rebuild the compiler from source.

Migration: replace the names in your scripts and in your CI setup.

0.7.21 — 22 September 2026

Unproved code no longer runs by default

What appeared

• Environment variables and command-line arguments in plans. The orders were in the language's vocabulary, but the runtime answered FLANG_IO_UNKNOWN.

вариант «Сделать» с поручение равным (вариант «Прочитать переменную среды» с имя равным "HOME")

The reply is «Значение среды» with field значение, or «Переменной среды нет» as its own variant — not an empty string. A plan's arguments are whatever follows --:

$ flang io script.fscript -- build --verbose

Deny with --no-env, --no-args.

• Terminal output. «Показать» draws a frame, «Ждать событие» waits for a key:

вариант «Сделать» с поручение равным (вариант «Показать» с место равным "экран" и текст равным кадр)
вариант «Сделать» с поручение равным (вариант «Ждать событие» с срок равным 5000)

A key arrives as «Случилось» with fields откуда and значение; a timeout as «Срок вышел». Key names: ввод, пробел, таб, возврат, выход, вверх, вниз, влево, вправо; a printable character arrives as itself.

Working example: docs/examples/io/progress-bar-on-screen.flang. The frame goes to /dev/tty, not stdout — stdout carries the plan's JSON result. With no terminal (pipe, file, CI) the answer is the same FLANG_IO_NO_SCREEN as before. Ctrl-C still kills the program. Deny with --no-screen.

• bootstrap/flang io scripts/four-coverages.fscript --plan Measure --timeout 900000 prints four coverages separately, each with its own line saying what it is not, and every number carries a date and a commit.

What changed

• The independent checker no longer accepts a false proof. Two holes: arguments were substituted sequentially rather than simultaneously, and body substitution did not check for name capture. Neither 529 mutation probes nor four tree gates had caught them.
• The same checker no longer rejects honest records — the verdict depended on the order the blocks were printed in.
• The share of places the checker replays independently is 650 of 650. Not one place is taken on the kernel's word any more; there used to be 12 premises and 4 steps.

What broke

• flang run and flang io exit with code 3 when a function's promise is not proved. Such a program used to run and exit 0.

$ flang run price.flang --function 'Скидка' --args '{"цена": 100, "скидка": 150}'
не доказано: утверждений 1: доказано 0, сетка 1 — запуск только по явному согласию: --trust
exit 3

Migration: add --trust and the verdict is not computed at all.

Affected: scripts calling flang run or flang io on programs where обеспечивает is backed by examples only. Check in advance with flang check --proof <file> — a summary reading «доказано 0, сетка N» means the program falls under the new rule.

0.7.20 — 18 September 2026

The compiler's own proof is fully replayed: 650 places of 650

What appeared

• For the first time bootstrap/flang io scripts/provability.fscript --plan Verdict --timeout 900000 prints ДОКАЗУЕМ against a 100 % gate: every one of the 650 obligations in the compiler's own proof records was replayed by an independent C program, with nothing taken on the compiler's word. Before this some places were accepted on trust and the gate stood lower.
• Discharging a precondition (требует) at a call site is now printed into the record and replayed as well: the second share, the one that counts preconditions, is 652 of 652.
• The seed reprint carried kernel fixes into the built compiler: a call's precondition is no longer discharged by the declared type of its argument; требует accepts a quantifier over list elements; a written-out list, отобразить and an applied function label gained the rights they lacked; the kernel now prints the justification it used to compute and drop.

What changed

• The provability gate was raised from 95 % to 100 % — the owner's word. Until the reprint the verdict at that gate honestly printed НЕ ДОКАЗУЕМ.
• package.json is gone from the tree: project settings are read from .flangrc, and a guard keeps the file from coming back.
• The inference rules were judged again by a foreign kernel — Lean 4.34.0: 109 rule rows, 107 of them with a lemma, and on 1 488 replayed derivations the checker and Lean disagreed 0 times.

What broke

• The proof still covers the source, not the printed program: nothing checks that flang emit --target c printed the program that was verified. Coq, Lean and Idris have the same gap.
• The checker is itself trusted code: 7 531 lines of C code against a ratchet ceiling of 7 603, its rules cross-checked by Lean, but not itself proved.
• Time, side effects and processes still have no rules: 414 places in the tree need them, and only the first three steps are written down.
• 100 % is the share of places in the compiler's own proof, not «all programs are proved». The verdict about your program comes from flang check --proof and the checker beside it.

0.7.19 — 13 September 2026

Quantifiers reached the built compiler

What appeared

• You can now say «for every element of this list», and the compiler will prove it. Previously a quantifier could bind only plain names, and there was no way to speak about list elements. Nested quantifiers work too: «for each element and for each other element».
• Induction over your own declared type. Proving something about your own type by case analysis was impossible before — the rules knew only built-in types.
• A statement can stand on its own rather than beside a function: «statement «the length of any list is non-negative»». Such statements now reach both the machine report and the proved-share ledger.
• A proof step can be named in words: a theorem step names its rule and premises, and the kernel checks that the naming holds. Steps used to be anonymous.
• The compiler emits TypeScript, and the help text finally says so. Emission worked before, but flang --help was silent about the tenth target: the seed lagged the sources by one line.

What changed

• The kernel now has thirteen inference rules instead of twelve — one was added for existence with a witness. There are 284 theorems in the language tree.
• Installation via Homebrew is now checked end to end. Five breakages were found and fixed: the help named nine emit targets while ten runtimes shipped; error messages crashed on their own under older Apple shells; the version check demanded a one-line answer that is deliberately two lines; the directory count did not follow symlinks, and Homebrew installs exactly symlinks.
• The English releases page pointed to the journals one level above the site root — four links led nowhere.
• Editing the task tracker no longer rebuilds the compiler in the cloud: two jobs used to run on every push regardless of content.

What broke

• The independently replayed share did not grow: 629 obligations of 651, the same 96.62 %. Reprinting the seed brought new kernel abilities, not a larger share. Places where the checker takes the compiler's word remain 12 premises and 4 steps.
• More must be trusted than yesterday: the deciding part of the kernel grew from 4669 lines to 4796. Quantifiers live there by construction and cannot be moved out. The work order to bring that number below 4000 remains unmet.
• The logic still knows nothing about state over time, side effects or concurrency. Work on those three has started but did not make this release.
• The proof applies to flang check and does not cover the built binary: nothing verifies that the emitted C matches the source program. Coq, Lean and Idris have the same gap.

0.7.18 — 12 September 2026

The checker got stricter, and the tree got clearer

What appeared

• The independent checker now replays 629 of 651 obligations instead of 625 — 96.62 %. Places where it takes the compiler's word dropped from 16 to 12. The gain came from replaying steps, not from computing: the «closed by computing» class stayed at 6.
• The terminal tutorial grew from five lessons to twelve. It no longer asks you to type a whole program: it gives the text with gaps and asks for them one at a time, saying after each line what it understood. A name may be written with guillemets «Удвоить» or plain quotes — the compiler accepts both, and the tutorial no longer argues about it.
• Obligations of a free statement (one that stands outside a function) now reach the machine report flang check --proof --json. They used to be filtered out in three places, so neither the proved-share ledger nor the site numbers could see them.

What changed

• Example programs moved from examples/ to docs/examples/: 200 programs in 24 directories. Working scripts are sorted into eight folders — the root of scripts/ now holds 13 files instead of 136. Benchmarks that had not been run in a long time were removed; the live ones moved to docs/benchmarks/ with English names.
• Browser samples (web/) became what they always were — examples: they now live in docs/examples/web/.
• package.json stays, but three fields no tool reads were removed. It is not there for npm: it is the single place from which the release, two guards, the Homebrew formula and the site build take the version, licence and URLs.
• The name-collision guard caught a real one: the type «Документ» is declared both in the JSON reader and in the language server, and a probe pulled both into one program. The cause was fixed rather than the guard — the probe lost an import it never used.

What broke

• Quantifiers over list elements, nested quantifiers, induction over your own declared type, statements outside functions, and proof steps named by a human did NOT make this release. They are written and checked, but they reach the built compiler only by reprinting the seed, which is still running. They will ship in the next release.
• The proof still applies to flang check and does not cover the built binary: nothing verifies that the emitted C matches the source program. Coq, Lean and Idris have the same gap.
• The example ledger (ведомость-примеров.txt) still holds the old paths: the walker that prints it runs for two hours forty minutes and has never finished — neither here nor in CI. It cannot be rewritten by hand: the check is a line-by-line diff, and the line order there is the walk order.

0.7.17 — 11 September 2026

The language passed its own provability check

What appeared

• ./ярлык доказуемость answers PROVABLE for the first time. How it works: when the compiler checks a program, it writes down which claim was proved and by which steps. A separate C program, written without reference to the compiler, takes the source and that record and repeats every step itself. 625 of 651 obligations were repeated — 96 %.
• The check «the checking program does not compute instead of repeating steps» no longer looks for a function name in the code. It runs a real source + record pair that contains goals provable only by rewriting; an honest checker must refuse them. 34 kinds of obligation sit under that check.
• There are now 401 forged records. Each lies in its own way: a swapped function body, a reference to a prohibition instead of a rule, subtraction passed off as addition, a line number that misses the declaration. None was accepted. We do not claim the checker is correct — we show 401 attempts to fool it.
• 88 inference rules were checked by a second, independent system — Lean 4. Our rule text sits verbatim next to each lemma so a human can compare by eye. Eight deliberately broken rules were all rejected.
• flangtutor, a terminal tutorial in the spirit of vimtutor, is now part of the package. Five lessons; answers are judged by the real compiler. Installed alongside flang by Homebrew and asdf.
• The record-freshness check now tells a deliberately corrupted record from one that merely lags the compiler, and refuses to measure with a stale binary.

What changed

• Share of obligations repeated by the independent program: 79.88 % → 96.01 %. The gain came from repeating steps, not from computing: places closed by computation went down, 8 → 6.
• Lean found a wrong rule of ours and it is fixed. The rule about adding the same value to both sides of an inequality required the addend to be «bounded», and that word also allowed bounded-above only — i.e. negative infinity. One word separated the working rule from the false one.
• The type нат is now неотрицательное (non-negative). The old name stays a synonym until 1.0.
• flang package works again. It had been broken on every input since 29 August: a two-argument function was called with one.

What broke

• The proof applies to flang check and does NOT cover the built binary: nothing checks that the emitted C matches the source program. Coq, Lean and Idris have the same gap. How we intend to close it is in ADR-0030: check each run of the printer rather than the printer itself.
• What the logic can and cannot prove was measured by running it. «The total is not less than the goods» over addition — proved. «A discount cannot make the price negative» over subtraction with a precondition — declared, not proved. The logic knows nothing about state over time, side effects or concurrency.
• flang must not be used for medical, avionic or space software. Those require process certification: a trail from requirement to code and test, qualified tools, proved response-time bounds, behaviour under hardware failure. We have none of that, and percentages do not replace it. See ADR-0031.
• The release archive is not byte-identical between a local build and the GitHub pipeline build, although it is assembled by a deliberately reproducible recipe.

0.7.16 — 9 September 2026

The checker replays a derivation of a type fact; the road to the end is measured place by place

What appeared

• A DERIVATION REPLAY: the independent checker now replays a recorded derivation of a type fact step by step, rather than trusting a rule name. Each step's conclusion is written as a formula of the language and compared sign for sign; the block's goal is checked AGAINST THE SOURCE rather than taken from the record; every premise is checked on its merits (the line must be an argument declaration, an assumption, or the body of the function in question); names marked in the rule list as prohibitions are rejected. Decision ADR-0022: a type fact travels in the record as a DERIVATION, not as an axiom and not as a rule name.
• Forgery probes went from 200 to 219: nineteen new ones catch a lie inside the derivation block — a foreign goal, a line number that misses the declaration, a missing premise, the wrong premise, reordered steps, an unfolding that is not the body, an unterminated derivation, a name outside the rule list, subtraction passed off as a sum, a reference to a prohibition instead of a rule. No forgery was accepted and no honest record rejected.
• flangtutor, a guided tour of the language in the spirit of vimtutor: five lessons in increasing order, from module and function to postcondition and proof report. The learner's answer is judged by the REAL compiler — parsing, types, termination, examples — not by string comparison. Progress is remembered and an interrupted session resumes.
• Ctrl+L in the shell clears the screen and puts the typed line back. The key worked before but no check held it in place; now both halves are checked.
• flang package works again. It had been broken on every input since 29 August: the ledger was called with one argument against a two-argument function. Verified end to end: flang new creates a package, flang package builds it, the package imports.
• FLANG_MODULE_ROOT stops module lookup from climbing above the named root. Until now lookup walked ABOVE the tree root and an ancestor file one directory up beat the language library — six live cases, caught by no check.
• The type нат is now неотрицательное (non-negative). The abbreviation did not read; the old name stays a synonym until 1.0.

What changed

• The share of the corpus verified by the independent checker: 517 / 651 = 79.42 % → 520 / 651 = 79.88 %. The gain comes from two new printers; the denominator did not move.
• The Elixir target no longer emits a dead result line per postcondition — seventeen warnings in one file went to zero.
• Internal project words are out of reader-facing pages: thirteen places rewritten in plain words. Two lines were kept — they quote the compiler's own output verbatim, and rewriting them would misreport what the reader will see.
• Broken links in the tree: 1947 → 18. The check now tells a record of the past (a completed task, a dated report) from a promise about the present, and prints how many it skipped instead of hiding it.
• The derivation rule list grew to 71 rows in two notations, logical and categorical, checked against the kernel code row by row.

What broke

• The verdict is still NOT PROVABLE: three checks of four agree, the share is 79.88 % against a 95 % threshold.
• The road to the end is measured place by place: NOT ONE place is unreachable, and the ceiling of engineering work is 643 / 651 = 98.77 %. The last eight places are not work but a decision about what the number promises.
• Found during the release and not hidden: the release archive is not byte-identical between a local build and the pipeline build, although it is assembled by a deliberately reproducible recipe. The promise «build it yourself and compare» does not hold today.

0.7.15 — 8 September 2026

The calculator is gone from the checker: the independent-verification gate is closed

What appeared

• GATE G7 IS CLOSED. The step that PROVED a claim by computing it, instead of replaying the recorded moves, is gone from the checker. Gone from both places: removing it from one, the work was immediately picked up by the second (the половина_закрыта door, тождественны at depth 6), while a grep-by-name check printed zero. The forgery sentinel has been separated from the prover and stays. Sign-for-sign identity and closed arithmetic are kept.
• The gate's calculator check is NO LONGER A GREP BY NAME but a run against a live source+record pair. Two of its goals are provable only by rewriting the body through laws, and the record holds no moves at all, so an honest checker must leave them on the kernel's word and name them. The trap is TWO-SIDED: a third goal closes by sign-for-sign identity and must stay closed, otherwise a checker broken down to «I prove nothing» would pass too. Renaming a function can no longer evade the check.
• bootstrap/flang io scripts/provability.fscript --plan Verdict --timeout 900000 now runs FOUR checks and prints all four with numbers, whatever the earlier ones answered. It used to short-circuit. A sentinel that does not run is not a sentinel.
• A manifest of the forgery set, 31 rows, each class confirmed by reading the source header. A ratchet holds two numbers: how many forgeries are declared, and how many places of their honest halves are replayed. Check 4 goes red if the set weakens.
• A ledger of derivation rules, 71 rows in TWO notations, logical and categorical, checked against the kernel code row by row. Notation agreement is verifiable, not declared: each premise is numbered and the categorical form must name its position. Four sentinels with eight forgery probes. Decision ADR-0022: a type fact travels in the record as a DERIVATION, not as a rule name and not as an axiom.
• A settings file .flangrc and a choice of output language (ADR-0024). Key = value pairs, not JSON and not a program: the file is read before the language is ready to speak. Precedence: argument, environment, project file, home file, locale, default. The walk up stops at the first marker, so a distant file cannot override a near one.
• The shell prints its own build fingerprint as the second line of flang --version. Borrowed from iex: Tab completion, .clear, history across runs, paste without flicker (measured on one paste: 90 redraws before, 10 after).
• A tenth emit target, TypeScript. Both READMEs and the emit-promises sentinel count ten.

What changed

• The share denominator is NARROWED by ADR-0023: places unreachable in principle are taken out — the obligations of a record the checker rejects whole. Removal requires TWO signals at once, a manifest declaration AND a measured rejection: on one signal alone, corrupting a record would raise the share. The share is 517 / 651 = 79.42 % against 517 / 665 = 77.74 % under the old measure. The numerator did not change by a single place, and the balance is printed and checked.
• Comments removed from 58 flang files, 7429 lines fewer. Each file's code compared without comments byte for byte; flang check and flang test --ledger identical before and after.
• Broken links in the tree: 1947 → 18. The sentinel now tells a record of the past (a completed task, a dated report) from a promise about the present, and prints how many it skipped rather than hiding it. The exception list shrank rather than grew: 373 rows → 171.
• The GitHub release body is printed from docs/release-notes.json instead of a string in the pipeline. Version 0.7.14 had 168 characters of body for 93 commits. A release with no recorded notes is now refused.
• .claude and AGENTS.md moved to .ai/, README.ru.md to docs/.
• The version no longer lives in package.json: that file is printed from scripts/release/emit-package.flang.

What broke

• The share is incomparable with earlier releases for the second time running: 0.7.14 changed the numerator, 0.7.15 narrows the denominator. Both measures print a breakdown, and the denominator balance is verified by an instrument.
• flang package has been broken on every input since 29 August: a one-argument call against a two-argument function. Found by a run; the fix is one line and ships with the next seed reprint.
• Module lookup walks above the tree root, and an ancestor file one directory up beats the language library. The hole is named and measured: 20 names shadowable, 5 live shadowings. A sentinel sees it; the fix in the binary awaits a reprint.
• The verdict is still NOT PROVABLE: three checks of four agree, the share is 79.42 % against a 95 % threshold.

0.7.14 — 7 September 2026

The checker replays termination proofs itself

What appeared

• A totality certificate for COMPOSITION. The binary prints into the proof record the evidence «this function terminates because it has no recursion — only calls to already-terminating functions», and the independent checker replays that evidence (сверить_тотальность) instead of trusting the name of the rule. The replay does not depend on the order of blocks in the record: two passes plus cycle detection. The seed was reprinted and 82 corpus records were printed anew. Commits ff1dc5b7, cbac34ce, 7cd56073, fba02c9a.
• A totality certificate for RECURSION, kinds structure and step: termination by descent along a variant of an inductive type, and by a decreasing measure bounded below by zero. The binary prints the node with the full witness — decreasing argument, floor, turns, self-call — and the checker replays it. Honestly: on the current corpus the share gains about nothing, because the corpus proves termination of recursion over the built-in list by a type law rather than by these certificates; the ability landed as groundwork. Commits 4bfbd217, 5d73d391, d1bbbf94.
• A share-by-replay instrument: sh flang/proof/corpus-share.sh --проигрыванием. The numerator counts obligations the checker really replayed; the denominator counts ALL obligations of the corpus, including those taken on the kernel’s word and those of rejected records. No record drops out of the denominator. Commits 00a56ba5, 682006f5.
• Cross-module linking of the totality certificate (--набор, --зависимость): trust in a set of records is granted only through a replayed carrier. On the current corpus there are zero such sites — this landed as groundwork, not out of need. Commit 4743a313.

What changed

• The share ruler now counts differently, and the number is not comparable with earlier releases: steps «by example» and «by property», which the checker already verifies by computation, now go into the numerator and not only into the denominator. After the composition totality certificate the share is 47.33%, after crediting what is verified on the merits — 60.78%; the trusted base does not grow and no reprint is needed. The share printout breaks the number down: by moves, and on the merits. Commit f5ca9e8f.
• Category theory moved: the flang/cat directory became flang/ct, its prose docs/ct. Commits acca80a3, 8142524b.
• // comments and duplicates were removed from 192 example files, and http.flang was rewritten as a data table instead of 55 near-identical entries. Commits bfd86834, 853d2f01, d2779328.

What broke

• The language is still NOT formally provable. A fallback calculator, перепиской, remains in the checker: it recomputes some goals rather than replaying the recorded moves. While it is there the доказуемость shortcut answers NOT PROVABLE, and the calculator cannot be removed partially — the share would collapse outright.
• The 95% threshold is not guaranteed on this corpus even in the limit: deliberate corpus forgeries are kept in the denominator (otherwise the share could be inflated) and can never enter the numerator, so the structural ceiling lies roughly between 91% and 96% — the threshold sits inside that bracket.

0.7.13 — 6 September 2026

The proof object: the checker verifies the kernel’s finished derivation instead of recomputing it

What appeared

• The binary itself now prints a replayable proof trace for five identity families — neighbours, reflexivity, length, element, compute. Until now only the checker could build the chain of moves. The first end-to-end run is green: the binary emits the trace, the independent checker replays it, «taken on the kernel’s word: 0». The seed was reprinted. Commits 2eb5633e, c3d17187.
• The «postcondition of the callee» technique: the checker builds an instance of the callee’s postcondition from the call site itself — arity, parameters substituted by arguments and the result by the node — and closes the goal by modus ponens, instead of the old name-plus-line binding. It catches a real forgery: a theorem claiming «the result equals 3» over a body that yields 0 used to pass with code 0 and now gives code 1. Commits e5a75366, d433f3b2.
• The moves «compute» (closed arithmetic such as «2 plus 2 equals 4») and «rewrite by form» (the length and element laws) are replayed by explicit primitives over оценить_терм rather than accepted on the kernel’s word. Commits a1f19f27, 269d3ccf, b0ef3a31.
• хеш256 became a built-in word of the language: SHA-256 is computed by the runtime of each of the nine emit targets, not by a flang library. Commits 5c90d6f7, ee3b0121.
• The js target got a Node host — flang/src/emit/js/flang_host_node.js. A program with an input/output plan, printed to JavaScript, now actually runs: nine kinds of orders out of twenty-two, with a clear refusal for the rest. Commit 7e7007a2.
• A plan executor for the python target landed in the tree — flang/src/emit/python/flang_io.py. The python target still refuses to print a program WITH a plan (FLANG_PLAN_UNSUPPORTED): the executor is waiting for the emitter. Commit e84e290b.
• Three examples under real frameworks — examples/frameworks/: nestjs-orders, react-invoice, vue-roman. A proven core in flang is printed to JavaScript and runs under Nest, React and Vue; each example’s README states where the boundary lies: the decision is in flang, the socket and the rendering belong to the host framework. Commit 374e9aaa.
• ./ярлык доказуемость prints a single word — PROVABLE or NOT PROVABLE — from three numbers taken by a run, not from a judgement written into prose. Commit 7b03ee3a.
• ./ярлык версия X.Y.Z raises the version number in one source and propagates it to the derived places — package.json, the #define in C, the man page, the Homebrew formula; a guard reddens if any of them falls behind. Commits 3071b76c, d676ec12.

What changed

• The replayer now gates equality postconditions on the chain of moves. Previously a false move under an equality postcondition passed with code 3, indistinguishable from an honest one, because the replayer was called on zero lines; now such a move gives code 1. Commit 3931ae1a.
• Two checker complaints are closed: a premise under принцип … without an explicitly written теорема never reached the replayer (the moves beneath it were decoration), and вставить_вместо unconditionally wrapped the inserted body in one extra pair of parentheses, so on a compound condition no wording of the argument ever reached the goal. Commit 3cb04bcb.
• The seed can be re-sown quickly, without a full reprint, when flang/self is untouched. Commit d0060d56.
• The list of flang commands is checked against five places at once: the man page and both READMEs did not know the new command. Commit fb29de4d.
• The ninth emit target, elixir, came under CI supervision, and divergence between the nine targets on one program is now watched by a separate instrument. Commits 5a5e9a74, 532e6f2b.

What broke

• The language is NOT formally provable, and that is a machine verdict rather than an opinion: git grep -c перепиской flang/proof/checker/checker.c gives 10, not 0, and ./ярлык доказуемость answers NOT PROVABLE. Two of the criterion’s seven gates are taken.
• A narrow subclass of sites is not migrated: the «by declaration» route — 146 of 159 «proved» sites — prints only the name of the rule, with no chain of moves, so the replayer has nothing to replay.
• Paying for требует in the new technique is partial: a callee’s precondition counts as discharged only if it syntactically matched one of the caller’s own требует. Discharge by computation or by an если guard is not read by this wave — such sites are honestly rejected with code 1 rather than wrongly accepted.

0.7.12 — 6 September 2026

An install now carries the runtimes of all nine emit targets, not one

What appeared

• A walker over the flang/self examples, and a CI job around it: 4350 examples of 4445 are supervised. Before this nobody ran them file by file — zero in CI. The full run was taken end to end: 55 minutes 19 seconds, exit code 0, 12,530 examples. Commits a35a4b42, ec039e7f, 3690acf4.
• A second carrier for the «by case analysis» technique — algebra, with forgery probes. Commits e11ed933, bb1e15a8.
• Two checker rules: «start by construction» by value and not only by identity, and «unsatisfiable premise» — anything follows from incompatible assumptions. Counted by corpus records that is 28 of 86 against 30 of 86. Commits 2d58f99e, 3e2ac46c.
• The verdict cache printout names its hits and misses by number. Commit c137e8d5.

What changed

• The release archive now carries a runtime/<target>/ directory — 32 files, 2,435,747 bytes — and the Homebrew formula and the asdf plugin move its whole root into share/flang. Previously exactly one target of nine was installed: the other eight were promised by the man page, both READMEs and the binary’s own help, and did not work for whoever installed it. Commit 11295873.
• The verdict cache key is computed with SHA-256 instead of a polynomial: the old key, advertised at 59.79 bits, was forged in 3.6 seconds. Commit deea0d61.
• The corpus was reprinted with the current binary — 67 records. The checker-verified share went 13.75% → 17.77% (17.92% was expected; the difference is a shifted denominator): the share had been held down by stale records, not by the checker. Commits e1e362da, ed5de60a.
• The hole «moves without a theorem hide the debt» is closed on both halves: «closed by reduction» is checked against the source, and an empty «move end» no longer hides the debt. Commit 817be78a.
• «This number» was added to the proofterm import list — 1289 examples had never run at all. Commit a85c7bb4.
• The ninth emit target was added to five guards that did not see it; along the way it turned out that the cpp target escapes names by the c target’s list. Commit 9fb0f293.

What broke

• The language is still NOT formally provable: the checker replayed 30 corpus records of 86, against a gate threshold of 95%.
• CI builds and runs eight emit targets of nine; as of this release the ninth is only named by a number — it came under supervision in 0.7.13. Commit 6c0deb07.

0.7.11 — 5 September 2026

Supervision is back on dev, and guards prove by a run that they can redden

What appeared

• The .githooks/pre-push hook runs the cheap guards before a push and says out loud what it did NOT check. The full set costs about 134 runner minutes — a hook that long would be bypassed with --no-verify and would be worse than none. Installed with one command: git config core.hooksPath .githooks. Commit 1de3cf23.
• An instrument for «who has been shown by a run to redden»: a guard without a forgery probe is a guard that is trusted for nothing. Commits ff354a73, 69550a3e, dc24ffa3, 83a838b2.
• A census of «which guards CI never calls»: the number had been counted by hand, and it was wrong. Commits b29e8fa6, 3fa4c09f.
• A guard over the derived version numbers: the version string in the seed had been systematically falling behind the release; now the divergence reddens, and the version is checked against the release ARTEFACT rather than against a file lying next to it. Commits 2532b671, cf337f76.
• The proved-share ledger checks its own table against the tree and is wired into both the shortcut list and CI. Commits 1bfe1e7d, 5dba51a1, 2aa82f5c.

What changed

• The checker learned three rules: negation of a closed computation, the finiteness proviso taken as a premise, and «the goal follows from what was declared about the arguments». The checker-verified share of the corpus went 7.50% → 13.75%. Commits 25181b19, ee23dd75, f5d378a1.
• The last named hole in gate G2 is closed: the induction argument is taken BEFORE the colon. Separately, a false acceptance is closed — a type declaration was being read through a trailing comment — and with it five false alarms. A wider measurement gives 62 false alarms out of 923 for the old checker and 0 for the new one. Commits 002b20f6, a54d4b55, 56a8441c.
• CI runs on the dev branch again: nineteen jobs had checked none of 74 pushes. The CI build became twice as fast and the binary is cached. Commits 8f90f49a, 15e89235.
• Syncing the Homebrew tap is written into the release procedure: six releases in a row, 0.7.4 through 0.7.10, went out without it, and all that time brew install was installing 0.7.3. Commit db23eb3b.
• The 0.7.x release notes were taken from main wholesale: they had been written there and never came back to dev, because a release is made on main. Eleven versions were added and none rewritten. Commit 532468f2.

What broke

• The 0.7.11 archive never shipped, and this tag has no GitHub release. The release pipeline stopped at the step «check the archive hash against the Homebrew formula»: the formula at that tag still carried the sha256 of the 0.7.10 archive (825a2b5b…, the very one from v0.7.10) — ./ярлык версия deliberately does not touch sha256, it is written in by a separate commit after a dry run, and for 0.7.11 that commit was never made. The pipeline skipped the upload step; nothing broken went out, and the tag was not deleted.
• The language is still NOT formally provable: the checker-verified share of the corpus is 13.75% against a gate threshold of 95%. And at this point it is held down not by the checker’s rules but by stale corpus records — the measurement promises 17.92% from a reprint. Commit 7e369d98.
• Only 8 guards of 58 have been shown by a run that they can redden, and CI was trusting twenty of the unproven ones for nothing. Commit ff354a73.
• The guard census as of 5 September 2026: 56 guards, CI calls 29, twenty-seven are called by nobody. Commit 3fa4c09f.

0.7.10 — 4 September 2026

Hotfix: the live shell crashed on every line of input

What changed

• The REPL (flang with no arguments) answered FLANG_UNKNOWN_NAME: record has no field «scheduler header» on ANY input, including 1 плюс 1 — not just elaborate examples. Cause: a hand-rolled field list for the «Settings» record in flang_repl.c (used by the «c» target's emitter for every line of a live session) fell behind the shared field table by two names when the «c» target learned to emit processes. The fix landed on dev on September 3rd, but after the v0.7.3 tag was already cut — so the bug was live in that release.
• The seed's version string (FLANG_VERSION) had drifted three releases behind (0.7.0 instead of 0.7.3) — the same bug class already fixed once by the 0.7.1 hotfix, recurred, and is fixed again; a task now tracks preventing a fourth recurrence.

What broke

• The language is still NOT formally provable: 2 of the criterion's 7 gates are taken. In the meantime a real hole in the independent checker was found and fixed (hiding text behind a trailing comment went unchecked at one more site), checker-verified corpus share rose from 5.00% to 7.50%, and for the first time two independent prints of the same commit matched byte-for-byte — but no gate was closed outright by any of this.

0.7.9 — 4 September 2026

Tagged, publication stopped by the pipeline

What changed

• Same content that shipped as 0.7.10 — the sixth publication failure in a row in this chain (after v0.7.4-v0.7.8), before finding the real fix: release.yml's workflow_dispatch was never removed (only the old publish-npm.yml lost it), and a dry run on the branch gives the real hash without burning a tag. The pipeline stopped BEFORE publishing each time, nothing broken went out; the tag was not deleted, simply skipped.

0.7.8 — 4 September 2026

Tagged, publication stopped by the pipeline — deliberately

What changed

• Tagged on purpose with a known-wrong hash (the 0.7.7 archive's) to harvest the real 0.7.8 archive hash from the pipeline's own error text. Also found along the way: the pipeline requires the tag's version to exactly match package.json BEFORE building the archive — the version could not be left unchanged to keep a hash valid. The same content actually shipped as 0.7.9.

0.7.7 — 4 September 2026

Tagged, publication stopped by the pipeline — deliberately

What changed

• Tagged on purpose with a known-wrong hash (the 0.7.6 archive's) specifically to harvest the real 0.7.7 archive hash from the pipeline's own error text — the same technique already used twice tonight. The same content actually shipped as 0.7.8.

0.7.6 — 4 September 2026

Tagged, publication stopped by the pipeline

What changed

• The number in the Homebrew formula was the 0.7.5 archive's hash (the coordinator copied the pipeline-reported hash for the wrong content version) — its own build on the tag naturally diverged. The pipeline stopped BEFORE publishing, nothing broken went out. The tag was not deleted, simply skipped.

0.7.5 — 4 September 2026

Tagged, publication stopped by the pipeline

What changed

• Same content that shipped as 0.7.6: the Homebrew formula's sha256 was computed locally with the documented command, but the local archive build didn't byte-match what the pipeline produces (cause undiagnosed) — the pipeline stopped BEFORE publishing, nothing broken went out. The tag was not deleted, simply skipped.

0.7.4 — 4 September 2026

Tagged, publication stopped by the pipeline

What changed

• Same content that shipped as 0.7.5: the Homebrew formula's sha256 was still 0.7.3's, the release pipeline checked it against the archive it built on the tag itself, and stopped BEFORE publishing — the safeguard worked as intended, nothing broken went out. The tag was not deleted, simply skipped.

0.7.3 — 3 September 2026

The version hotfix finally reached publication

What changed

• The same version hotfix tagged as 0.7.1 and 0.7.2 is finally published: for both of those tags the hand-built archive didn't match what the release pipeline itself built (0.7.1 — a full mismatch; 0.7.2 — 4 bytes out of 4,447,763, cause never diagnosed), and the Homebrew formula failed verification. For 0.7.3 the sha256 was taken directly from the pipeline's own sha256sum rather than recomputed by hand — installation was verified end to end: download, hash check, build, flang --version.

0.7.2 — 3 September 2026

Tagged, but publication failed again

What changed

• A second attempt to publish the 0.7.1 version hotfix: the archive's real sha256 was taken from the pipeline rather than recomputed by hand. The build still diverged from the pipeline's own by 4 bytes out of 4,447,763 (cause never diagnosed) — the Homebrew formula failed verification. The tag was not deleted (deleting tags is forbidden here), simply skipped: it delivered nothing to anyone installing via Homebrew.

0.7.1 — 3 September 2026

Version hotfix — tagged, but publication didn't land

What changed

• flang --version answered “0.6.2” under the 0.7.0 release — two releases behind: the seed's version string was left un-bumped alongside package.json. Task 9959 fixes it. Also fixed along the way: the Homebrew formula's version (0.6.2 -> 0.7.0, missed in the first pass), the version shown on the site, and part of a CI job that was burning push-triggered hours running under no name.

What broke

• Publication under this tag did NOT land: the hand-built release archive didn't match what the release pipeline itself built, and the Homebrew formula failed its hash check. The tag was not deleted, simply skipped — this same fix was only successfully published as 0.7.3.

0.7.0 — 3 September 2026

The compiler was reprinted from scratch, and the release’s main work was finding our own self-deceptions

What appeared

• C++ became the ninth print target; regular expressions, sqlite and Redis drivers, TLS 1.3 and a package registry arrived.
• Files take three equal extensions; step and depth limits have their own flags; --no-check prints without checking, and check --быстро says plainly what it did not look at.

What changed

• The compiler was reprinted from scratch off the frozen trunk: the print took 12 hours 4 minutes, of which 10 hours 25 minutes (86 %) was the kernel-judgment stage.
• The release path completed end to end for the first time. Before, it never had: the archive step called a binary nobody built, and the 0.6.2 release was assembled by hand.

What broke

• The language is NOT formally provable: two of the criterion’s seven gates are taken — the kernel emits a proof object, and the size of the trusted base is named as a number.
• The kernel can prove a FALSEHOOD: unfolding a call substitutes an argument under a binder of the same name and prints “proved for ALL inputs” about a claim false on every input. Today’s corpus contains no such proof — measured, 0 of 240.
• The share of the corpus verified by the independent checker is 0.00 % as of the freeze. The previously quoted 0.83 % was overstated and has been withdrawn.
• Reprinting the compiler with the 0.7.0 seed needs --предел-глубины 200000: the built-in limit of 20 000 hits one machine-written postcondition line of 90 286 code points.

0.6.2 — 22 August 2026

The Homebrew install is fixed: the archive shipped a directory nobody could enter

What appeared

• The secure connection works for real: twelve runs with genuine response codes.
• The fold principle is strengthened with the already-traversed part of the list: +2 proved obligations, with a forgery and its honest half added alongside the rule.

What changed

• The two measures of string length are reduced to one. A memory corruption was found and closed along the way.
• Import discovery parses the file header rather than the whole file: 24% less memory, 5% less time.
• Two hand-written copies of list comparison were removed and three stale references to a long-lifted ban were fixed.

What broke

• Nothing. This release fixes the install broken in 0.6.0 and 0.6.1: the archive was packed with --mode=u=rw,go=r, which strips the traverse bit from DIRECTORIES too, so runtime-c arrived as drw-r--r-- and brew install failed with Errno::ENOENT: runtime-c/flang_cli.c. The cure is the letter X — --mode=u=rw,go=r,a+X. The command is corrected both in the formula and in the publish workflow.

0.6.1 — 22 August 2026

A compiler change that never reached the built compiler now goes red in half a second

What appeared

• A cheap check that the compiler sources match their C translation: sh scripts/bootstrap-reprint.sh --bystro. Previously a mismatch was caught only by the hour-long reprint, and over two days work reached the trunk four times carrying a rule the built compiler did not have. It is now visible immediately, on every push.
• Two new rules in the proof checker: case analysis over a goal's inner condition, and a rule for incompatible conditions. The gain is measured and written as a number in the kernel itself: +2 and +2 proved obligations across six library files.
• An octet pair of file orders: read and write a file as bytes rather than text. The text pair now refuses honestly on non-text instead of corrupting it silently, and a zero octet is legal text again — the refusal is only for malformed UTF-8.

What changed

• The name-collision check sees the whole closure: an import by name without a path is resolved through the registry, and instead of one file out of thirty-six it now looks at all of them. On this tree: 736 files, 56,345 declarations.
• The forgery check reads the whole directory rather than a list: 15 named forgeries became 24, and stopping at the first failure no longer hides the rest.
• «Ответить в соединение» no longer truncates content at the first zero byte: the length is taken from the value itself. Measured on the compiler's own source — the trunk was losing 47,184 bytes on flang/self/link.flang.

What broke

• The text file-read and file-write orders now refuse on binary content instead of returning a truncated result. Use the octet pair for binary.

0.6.0 — 22 August 2026

Long computations no longer hit a memory wall: 15.98 GiB became 0.0135

What appeared

• PostgreSQL login over scram-sha-256: SHA-1, HMAC, PBKDF2 and the SCRAM client are written in the language itself, and the login is verified by a run against a real PostgreSQL 17.10, not a stub.
• Three new inference rules in the proof checker. A finiteness caveat: NaN sits outside the order, every bound over it is false, and the caveat "while this is a number" is now read as a fact. Case analysis over a disjunction in an assumption: "A or B" is not split, it is taken apart into two cases, and the goal is accepted only when both close. And the goal "A and also B".
• Supervision of failed processes across the network: a node survives the death of its neighbour, and the lost work is taken over by the survivor. The loss is reported to the supervisor by the link layer, not by socket cleanup.
• A "Wire" module — the shared half of binary protocols over TCP, lifted out of the PostgreSQL driver. Of the driver's 83 functions only 39 were about PostgreSQL; the rest fit any binary protocol.
• Browser pages are written in the language itself: eight emit targets out of eight, and not a single line of JavaScript in the pages.
• A check for vacuous proofs. The library's 93 proved claims are sorted into four piles, and "proved" about something that holds for any function with the same signature is named for what it is instead of being counted alongside substantive claims.

What changed

• Memory no longer grows during a long computation. The interpreter is a loop, and its arena was released only at the very end: tail recursion cost 84 kilobytes per iteration. It is now released on every iteration. Over 200,000 iterations the peak went from 15.98 GiB to 0.0135 GiB, time from 25.3 to 13.5 seconds, and the peak no longer depends on the iteration count at all.
• Equality in a function body is allowed: the old ban turned out to be a stale restriction rather than a boundary of the language. Permission to compute is still not permission to infer — there is a forgery fixture for exactly that.
• The step ceiling for printing the compiler was raised from 40 million to a billion. After the new inference rules the compiler's check of itself no longer fit under the old one, and printing was cancelled outright.
• The JavaScript implementations of the checks are gone: the proof layer (4,958 lines), the emit and occupied-name checks (682 lines) and four files nobody called (836 lines). Printing the compiler to C needs Node at no step.
• Searching the documentation by refusal code finds 13 codes out of 13 — it used to find 0 of 13.

What broke

• The emit:check shortcut is gone: the emit check is done by pechat:check in the language itself, and occupied:check now calls scripts/guards/occupied-names-guard.flang instead of the removed JavaScript script.
• The shared half of the PostgreSQL driver moved into the "Wire" module. Programs that called «Знак байта», «Четыре октета», «Два октета» and their neighbours directly from the database module must now import "Wire".

0.5.1 — 19 August 2026

The macOS install is fixed: 0.5.0 did not build there for anyone

What appeared

• «Открыть соединение» — an order with which a program itself reaches a foreign service over a socket. Before it, no client to a database or to any binary-protocol service could be written in flang: a service could answer but not ask.
• All four network orders now use one word for the concept.
• A second door for a printed C program — МОДУЛЬ_enter — checks arguments against declared types. Before it, foreign code linked against the library got 1 for −3 on a нат argument and never knew.

What changed

• The npm package is named @digitable-lol/flang, not @digitable-lol/fts.
• The C files are compiler_flang.[ch] instead of kompilyator_flang.[ch]; the printed output shrank by 124 431 bytes.
• The build output is named flang, not flang_cli; the Homebrew formula and the asdf plugin accept both.

What broke

• Nothing previously promised. The binary still emits to C only and does not take composite values in --args; both limits are named on the install pages and in man.

0.5.0 — 18 August 2026

The compiler measures itself, and the emitted code got faster and leaner

What appeared

• Each of the eight emission targets is now also written in flang itself; js was the last one closed. No target is left without its own flang version.
• The proof report is computed by code written in flang itself: flang check --proof no longer calls the JavaScript implementation.
• The type вес — the segment from zero to infinity. Three operations over it are allowed, four refuse and show the pair they refused on.
• Exact decimals: money is computed without a binary fraction, and the binary handles it itself.
• The permission "safe to repeat" is now granted explicitly instead of being assumed.
• A dependency lock file: a program builds from it without the sources.
• Input and output grew directory listing and process spawning, and flang io distinguishes "found a problem" from "broke itself" by different exit codes.
• The documentation site builds from docs/ by one command, with no dependency at all.

What changed

• Emitted C got faster: link-time optimisation is on by default — that is 1.14× — and the type check is not emitted where the type is already proved: 4.9× on arithmetic, 1.6× together.
• The memory region in the C target learned to roll back: merge sort over four thousand numbers takes 3.5 MiB instead of 1655.
• The declared depth limit in WebAssembly became a limit: 7474 nested calls and the same refusal text as an ordinary run, instead of a dead tab at depth 60.
• Diagnostics quote the word of the surface the file is written in: 0 mismatches out of 186.
• The language server stopped answering an argument it did not understand with zero bytes and exit code 0.

What broke

• The word требует became a keyword. A program where that was a name of its own no longer parses.

0.4.8 — 9 August 2026

Subset and intersection: sets got words

What appeared

• Sets got words: containment and common part — and they work by a reason, not by a list.
• A declared measure: убывает <expression>. A loop is proved by it where the two free orderings were not enough.
• Logic is written infix: не, и притом, или.
• A character's code point became a number — that is exactly what strings were missing.
• A process has its own heap: a message travels into it as a copy, and exhausting the heap became a failure of the process, not the death of the program.
• A mailbox is bounded by a declared size, and overflow became a failure of the sender.
• The dictionary became logarithmic: a search tree with priority by the key's hash.

What changed

• Hot swap runs under a live scheduler, and state is carried over by a checked function.
• The compiler emitted into C now installs the run-time check that the measure decreases, and no longer loops where the JavaScript implementation refused.

What broke

• The word убывает became a keyword.

0.4.7 — 7 August 2026

Monad, failure as a value, polymorphism

What appeared

• The monad got a form: в монаде unfolds into a case analysis all the way down.
• The failure of "to number" became a value: a column of strings adds up without falling over.
• A number descends by a constant step — down to a checked floor.

What changed

• тотальная stopped promising more than is proved: where termination rests on a number, a run-time check that the measure decreases is emitted.
• The library collapsed along its types once polymorphism was closed; the second parameter found a defect in self-application.

0.4.6 — 7 August 2026

The binary talks to a human: check, shell, help, man

What appeared

• The installed binary became a tool for a human: flang check, help, version, a man page.
• A function became a value: the compiler replaces it with a tag and dispatches on tags, so the call graph stays finite and a function-value reached every emission target.
• The language got a dictionary.
• Logical operations arrived as functions — the word "и" is already taken in this language.

What changed

• Self-application understands polymorphism and higher order.
• Linking stopped losing the categorical layer at a file boundary: a proof used to survive it and should not have.

0.4.5 — 7 August 2026

A shell in the installed binary, input/output, and processes on BEAM

What appeared

• The shell is in the binary that installs ready-made: the language can be touched right after installation.
• The language learned to read a file and reach the network without ceasing to be pure.
• Supervision stopped being a declaration: a fallen process is brought back to the same start.
• Processes ran on a real BEAM through Elixir emission, and the comparison goes by the set of outcomes.
• Types became parametric — without that the monad could not be stated.

What changed

• The lexer became total throughout: the self-application layers stopped walking a string by position.
• Four tasks and the standard library became total.

0.4.4 — 6 August 2026

A language server, a functor with laws, concurrency

What appeared

• A language server for .flang: the same check as flang check, right in the buffer.
• Concurrency: atomicity per process rather than global, plus BEAM emission.
• The functor stopped being a word without a guarantee: it got laws, and they are checked.

What changed

• Bidirectional control characters are no longer emitted raw into java, csharp and elixir: substituting a source with an invisible mark is closed in every target.

0.4.3 — 6 August 2026

Vim highlighting ships in the package

What appeared

• Highlighting ships in the package: 154 words of the language, with role distinguishability checked.
• The flang repl shell: the language can be touched, not only run from a file.
• The built-in form "split … into characters" — a per-character pass became provable.

0.4.2 — 6 August 2026

Eight emission targets, and the compiler installs without Node

What appeared

• Emission into Java, C# and Elixir — eight targets in all.
• The compiler installs without Node: released C and an installer formula.

What changed

• The compiler written in flang itself emitted itself with no differences at all.
• The package description was five emission targets behind — fixed.

0.4.1 — 5 August 2026

The package's commands answer after installation

What changed

• After installation the commands printed zero bytes and exited 0: the entry-point guard compared paths as strings, while the installer places commands as symbolic links. Held down by a check that places the link the same way.

0.4.0 — 5 August 2026

First publication

What appeared

• The package carries the language together with the FTS tools: 327 files, 1.1 MB archived and 8.3 MB unpacked.
• Emission into C, Go, Rust and Python.
• Module linking: использует, plus selective import with только.
• Self-application: the lexer, the parser, type checking, totality analysis and C emission — written in flang itself.
• The emit command: emission into a target language from the command line.