Выпуски

Выпуск — это тег vX.Y.Z, а по нему архив и публикация пакета. Страница печатается из тегов: сколько тегов, столько записей, пропустить выпуск нельзя.

Ящика три: что появилось, что изменилось, что сломалось. Пустой ящик не печатается — «сломалось: ничего» на девяти выпусках подряд читателю ничего не сообщает.

Записи ниже написаны про язык, а не про работу над ним. Что приехало в ствол после последнего выпуска, показывает журнал вливаний; заголовки всех коммитов — журнал коммитов.

0.7.29 — 18 октября 2026

Готовые сборки и установка одной командой, законы категорий доказываются

Что появилось

• Готовые сборки для Linux и macOS, установка одной командой. Компилятор C и sudo не нужны: curl -fsSL https://raw.githubusercontent.com/digitable-lol/flang/main/install.sh | sh кладёт flang в ~/.local/bin и сверяет архив с SHA256SUMS выпуска. Есть и другие пути: brew install digitable-lol/tap/flang-package, asdf, пакеты deb и rpm.
• Песочница в браузере. На странице https://digitable-lol.github.io/flang/playground.html программа и силлогизм проверяются прямо во вкладке: компилятор собран в WebAssembly, ставить ничего не нужно.
• Установленный flang находит стандартную библиотеку. использует «Lists» только «Длина» работает в программе из любого каталога: библиотека лежит в share/flang/stdlib рядом с двоичным. Раньше это работало только внутри клона репозитория.
• Законы моноида, функтора, изоморфизма и естественного преобразования доказывает ядро — для всех значений, а не на сетке. check --proof печатает их отдельным разделом, например на flang/ct/yoneda-preorder.flang: законов утверждениями 9: доказано ядром 9, не доказано 0, в --json это поле lawClaims. Недоказанный закон назван поимённо. Законы монады пока считаются на сетке.
• flang test исполняет блоки прогон и сверяет их ожидания. Каждый блок считается примером: неверное ожидание — код 1 и сообщение у процесса «Счётчик» состояние {"всего":5}, а ожидалось {"всего":999}.
• check --proof печатает ход доказательства у большинства утверждений: какое поле или какой вызов раскрыт и на какой строке исходника, например ход 1 поля ⟨«Пополнить» от ( счёт ) и сумма⟩ строка 15 …. У части утверждений пока только имя правила.
• Свойства «всегда» для процессов проверяются перебором конечной модели. Модель — процессы, их состояния и правила «получив письмо, перейти и отправить письма»; перебор обходит все порядки до заданной глубины. Ответ — либо кратчайший встречный прогон, либо «не нарушено … это не доказательство». Для модели flang/concurrency/temporal/models/deadlock.flang ответ — НАРУШЕНО, встречный прогон, шагов 6. Обе проверяющие программы (на C и на Lean 4) переигрывают такие записи сами: ПЕРЕБОР СВЕРЕН: встречный прогон переигран, шагов 6, в конце свойство «без тупика» ложно.
• Напечатанный C сверяется с эталоном. flang run-script translation:validate печатает примеры в C, собирает их и сравнивает ответы программ с ответами эталонной семантики на Lean 4: СООТВЕТСТВИЕ ПРОВЕРЕНО для 146 функций, вне валидации 4 … расхождений 0. Шесть нарочно испорченных версий напечатанного C она отвергает.
• Грамматика русского предложения на типизированных словах. flang run flang/ct/russian/parse.flang --function «Разобрать» --args '{"предложение":"мама читает книгу"}' отвечает грамматично: … связи: мама—читает, читает—книгу, а на «мама читает книга» — не грамматично: неверный падеж.
• Юникод 17 в стандартной библиотеке: нормализация (NFC, NFD), деление на графемы, сравнение без учёта регистра и явное раскодирование байтов. «Графемы» от "👨‍👩‍👧🇷🇺" — две графемы; «Равны без учёта регистра» от "STRASSE" и "straße" — да; «Раскодировать байты» от "UTF-8" и [104, 255] — отказ с местом 2 и причиной «байт не может начинать знак UTF-8».
• В оболочке flang repl можно писать утверждения, теоремы и силлогизмы. Оболочка сразу отвечает: утверждение «сложение перестановочно»: доказано (код 0), «опровергнуто» с контрпримером или «не доказано» с причиной.
• Эталонная семантика ядра языка записана на Lean 4, и для каждого шага, который переигрывает независимая проверяющая программа, на Lean доказано, что шаг корректен.

Что изменилось

• Экспортированная функция может звать скрытого помощника своего модуля. Раньше программа, которая подключала такой модуль, не проходила check; теперь проходит, а прямой вызов скрытой функции — ошибка FLANG_UNKNOWN_NAME: «её объявляет …, но не экспортирует».
• Вложенный объект — понятная ошибка вместо падения. Строка вложен объект даёт FLANG_PARSE … старое слово, программу из него не составить: вложенную запись объявите объектом и сошлитесь полем.
• Ошибки связывания называют файл, а не только строку и столбец.
• make install из клона репозитория пока не кладёт стандартную библиотеку — программа с использует «Lists» вне клона библиотеку не найдёт. Ставьте flang через install.sh, brew, asdf, deb или rpm: там библиотека есть.

Что сломалось

• run на программе, которая не проходит проверку, отвечает кодом 1, а не 3. То же с --на-веру: согласие на недоказанное не снимает ошибок разбора, связывания и типов. Если скрипт ждал код 3, проверяйте ненулевой код или исправьте ошибку из сообщения.
• Имя, которого нет в списке только, теперь ошибка FLANG_UNKNOWN_NAME при любом порядке строк использует. Раньше оно иногда проходило, если тот же модуль ввозил шире другой файл. Впишите имя в список только или уберите вызов.
• check --proof отвечает кодом 3, если часть утверждений держится только на примерах или на сетке значений. Раньше это был код 0 со словами «проверено с опорой». Например, на flang/stdlib/lists.flang (42 доказано, 24 на сетке) теперь НЕ ДОКАЗАНО — ОПОРА НЕ СУДИЛАСЬ и код 3. Если сборка считала успехом только 0, докажите оставшиеся утверждения или примите 3 как «проверено не всё».

0.7.28 — 14 октября 2026

Примеры в законах проверяются, ошибки в категориях находятся при компиляции

Что появилось

• flang test и flang check прогоняют примеры внутри блока закон. Раньше такие примеры не запускались вовсе, и неверное ожидание в них проходило молча. Теперь пример с неверным ожиданием даёт код 1, а сообщение называет закон, пример, ожидаемое и полученное значение: ожидалось {"номер":777}, получено {"номер":500}.
• check проверяет, как собрана категория. Стрелка, которой нет среди объявленных, стрелка, названная дважды, композиция через стрелку не из этой категории, концы стрелок, которые не сходятся, — всё это теперь ошибка с кодом 1 и номером строки. Например: FLANG_CATEGORY_UNKNOWN_ARROW в файле warehouse.flang, строка 9, столбец 1: категория «Склад»: стрелки «потерять» не объявлено.
• check --proof объясняет, почему не доказал равенство из длинной цепочки вызовов. Подстановка доказанных свойств функций делает не больше 64 шагов. Если их не хватило, утверждение остаётся недоказанным, и ответ говорит прямо: переписка доказанными равенствами исчерпала «Предел переписки» — 64 шага. Раньше было только «объявлено, не доказано» без причины.
• Обе проверяющие программы (на C и на Lean 4) перепроверяют утверждения с квантором внутри и притом и если. Такие утверждения ядро доказывало и раньше, теперь их доказательство перепроверяется независимо.

Что изменилось

• Файл с категориями, где все законы проверены, проходит check с кодом 0. Раньше любой такой файл получал код 2 с припиской, что устройство категорий не проверяется. Из 25 примеров в flang/ct с кодом 0 теперь проходят 16, было 7. Остальные 9 получают код 2 и называют закон, который не удалось проверить.
• check --proof по стандартной библиотеке стал немного быстрее. Ядро берёт доказанные свойства только у тех функций, которые встречаются в доказываемом утверждении. На 55 файлах flang/stdlib суммарное время 5773 с у 0.7.27 и 5518 с теперь, то есть на 4 % меньше; результаты проверки те же.

Что сломалось

• Неверный пример в блоке закон теперь роняет test и check с кодом 1. Исправьте ожидаемое значение в примере или саму функцию: сообщение называет оба значения.
• Ошибка в устройстве категории — теперь код 1 у check, а не 2. Объявите недостающую стрелку через морфизм или уберите её из блока категория; повторную строку удалите.

0.7.27 — 14 октября 2026

Доказательства по-взрослому: алгебра, завершение рекурсии, формулы в LaTeX; HTTPS без curl

Что появилось

• Ядро доказывает алгебраические тождества над целыми. check --proof раскрывает обе стороны равенства в многочлен и сравнивает их. Это аналог тактики ring в Lean. Например, (a + b)·(a + b) = a·a + a·b + b·a + b·b доказывается для всех точных целых a и b. Для число, то есть для double, такие законы ложны, поэтому там будет отказ с объяснением.
• Доказательства перепроверяют две независимые программы, на C и на Lean 4. Ядро записывает доказательство в файл, а обе программы перепроверяют его каждая по-своему. Если ядро ошибётся или запись подделают, это поймают. Что перепроверить не удалось, check --proof называет прямо. Обе проверки идут в CI на каждом пуше.
• Компилятор доказывает, что рекурсия завершается. Пишете у функции убывает н, и check либо доказывает, что н уменьшается при каждом вызове, либо отказывает с кодом FLANG_NOT_TOTAL. Так, н минус 1 на неотрицательных доказывается, а шаг вида 3·н + 1 (Коллатц) отвергается сразу, ещё до запуска.
• Доказанное свойство функции используется в других доказательствах. Если доказано, что f(x) равно какому-то выражению, ядро подставит это выражение везде, где встретится вызов f. Это аналог simp. Цепочка из 18 вложенных вызовов доказывается.
• Формулы можно писать как в учебнике. formula:read '∀ a ∈ ℤ, ∀ b ∈ ℤ, a + b = b + a' или та же формула в LaTeX превращается в утверждение flang, и его сразу проверяет ядро. Работает и обратно: formula:print файл.flang печатает утверждения файла как формулы и как LaTeX. ℕ означает точные целые, ℤ — 53-битные целые (переводчик об этом предупреждает), ℚ≥0 — точные дроби. ℝ и ℂ не поддерживаются: double не подчиняется законам поля.
• Длинное выражение можно переносить на новую строку внутри круглых скобок. Отступ продолжения не важен, ошибка указывает настоящие строку и столбец.
• Законы моноида, функтора, монады и изоморфизма проверяются при компиляции. Компилятор подставляет набор значений и ищет контрпример. Нарушенный закон даёт код 1, непроверенный — код 2. Это проверка на примерах, а не доказательство, и компилятор пишет это прямо. В flang/ct добавлено восемь примеров по теории категорий: произведение, копроизведение, пулбэк, сопряжение, лемма Йонеды на предпорядке, моноидальная категория, Maybe как моноид, стрелки Клейсли.
• HTTPS работает без curl. Клиент TLS 1.3 написан на flang и встроен в двоичный файл. Корневые сертификаты берутся из системы или из --trust-roots файл.pem. Добавлены отправка и приём UDP.
• Скрипты (.fscript) компилируются в C, Go, Rust и Python. flang_cli --plan <имя> запускает план в выбранном языке. Работают файлы, каталоги, переменные среды и аргументы. Остальные операции пока отвечают ошибкой FLANG_IO_NOT_WIRED.
• Сообщения компилятора по-английски. Задайте FLANG_LANG=en или language = en в .flangrc. Переводы лежат в обычной таблице flang/messages/catalog.tsv.
• Сгенерированный код проверяет типы на входе. Во всех десяти целевых языках программа отвергает вход, который не подходит под объявленный тип. Например, отрицательное число там, где объявлено неотрицательное.

Что изменилось

• Ошибка связывания модулей называет файл: сообщение начинается с в файле <путь>:.

Что сломалось

• HTTPS больше не вызывает curl. Если двоичный собран без встроенного клиента TLS (в том числе flang emit --repl), запрос по https отвечает FLANG_IO_NO_TLS. Отключить проверку сертификатов нельзя.
• Функция с убывает, у которой мера не уменьшается, теперь не проходит check (FLANG_NOT_TOTAL, код 1). Раньше она падала только при запуске.
• Конфликт имён при импорте теперь ошибка. Это случай, когда импортированная функция зовёт скрытого помощника своего модуля, а в другом файле есть одноимённый. Ошибка — FLANG_DUPLICATE_NAME. Чтобы исправить, добавьте помощника в список только или переименуйте его.
• Неверный закон моноида, монады или функтора — теперь код 1 у check. Раньше такие законы не проверялись.
• Неверный по типу вход сгенерированной программы — теперь FLANG_TYPE во всех целевых языках.

0.7.26 — 11 октября 2026

TLS на языке, случайность у хозяина, цена до прогона, кеш ядра и второй сличитель на Lean

Что появилось

• TLS 1.3 собран на языке и работает напечатанным (ADR-0078). flang/stdlib/tls-client.flang и certificate-path.flang: рукопожатие, проверка подписи сервера RSA-PSS (все 60 векторов pss-vect.txt приняты, подделки отвергнуты), цепочка до корня, срок, basicConstraints и имя узла — живой узел www.google.com до GTS Root R1. Поручение «Запросить» по https по-прежнему исполняет curl: решение названо, не умолчано.
• Хозяин отдаёт октеты из системного источника случайности (ADR-0077): поручение «Случайные октеты» с полем «сколько», отклик «Октеты». Главный довод ADR-0007 «секрет взять неоткуда» снят.
• Точное целое и точное дробное печатаются во все десять целей — рантаймы каждой цели считают их сами; целая часть — встроенная одноместная форма (ADR-0074); остаток над точным целым; пробы сверяют ответ толкователя с десятью целями байт в байт.
• Цена функции известна до прогона (ADR-0083): flang run --cost и поле cost у бегуна печатают границу шагов и памяти от размеров входа.
• Кеш ответов ядра между прогонами в подписанном каталоге (ADR-0080); памятка одного прогона (ADR-0051) стала памятью между прогонами.
• Второй сличитель записей — на Lean 4 (ADR-0076), сверен с сличителем на C; доказанным считается только то, что сличитель проиграл (ADR-0073); check --proof говорит, сколько проиграно.
• Правила ядра: индукция по отрезку, уплотнение целого и перебор конечной суммы (ADR-0075: Инд5, Инд6, Цел3) и переписка цели по доказанному равенству с квантором внутри формулы (ADR-0084: Переп1, Скл1–Скл3, Св2) — каждое с леммой в Lean и ловушкой.
• Нормальный параллелизм (ADR-0072): пул, чистое отображение и доказанный моноид; напечатанный C, Go, Java, C# и Elixir отображают и сворачивают список кусками; ядро судит законы моноида и помечает свёртки, которые режет.
• Чужой язык входит через недоверенного переводчика (ADR-0058): циклы, присваивания, вызовы и структуры C переводятся на flang и судятся ядром.
• Напечатанный код следует канону цели (ADR-0081): форматтер и линтер каждой из десяти целей принимают печать без правки; C и C++ раскладываются как clang-format LLVM, C# — как dotnet format.
• DESCRIPTION.md — зеркало языка: описание называет каждое слово лексера, каждую команду flang --help и каждый ключ настроек, сторож переписи это держит, а тело выпуска перечисляет изменённые разделы описания.
• Разбор случаев в сверщике читает больше тел и связывает атомы: допущения требует и проигранные обещания вызываемых — факты, длины считаются и делятся по половинам; пользовательская программа greeting теперь проигрывается сверщиком.

Что изменилось

• Лицензия живёт в одном файле LICENSE: строки SPDX сняты из исходников (112 файлов), сторож лицензий проверяет один корневой файл.
• Семя перепечатано дважды партией после 0.7.26: печать своим печатником, вторая печать — неподвижная точка (compiler_flang.c 43 917 383 байта).
• Сторож чисел сайта меряет то же, что печатает numbers:build; числа корпуса на сайте пересняты на нынешнем дереве.
• Замок пакетов: каждая форма зависимости доходит до файла замка; разрешение реестра доказано корпусом и подлогом.
• Сообщения check называют отчёт о доказательстве простыми словами; страница реестра печатается без внутренних слов.
• Сторожа переписей — планы на flang, доказанные ядром, а не оболочка: перепись рукописных списков, перепись судей, перепись незваных проверок.

Что сломалось

• Запись, в которой ничего не доказано, отвечает кодом 3, а не 0 — сличитель больше не молчит на пустом.
• Имя модуля второго сличителя и код подлога рукописных списков — английские слова; старые имена не читаются.
• Ядро отказывает в индукции, если имя образца затеняет параметр — программы, жившие на этой дыре, перестанут доказываться.

0.7.25 — 6 октября 2026

Точное целое и точное дробное, предел потомку от поручения, страница реестра

Что появилось

• Точное целое — свой тип, не новое имя числа (ADR-0036; задачи 1908, 1412, 1413). точное целое складывается, вычитается, умножается и сравнивается без потолка 2^53; значение — список разрядов по основанию 2^22 без знака, канон (без старших нулей) держится при каждом действии, литерал не в каноне отвергается типизатором. Разрядное сложение напечатано во все десять целей печати. Ассоциативность сложения над ним доказывается правилом ядра — первым правилом кольца, у которого есть лемма в Lean и подлоги в пробах.
• Точное дробное (ADR-0062; задача 5243). Пара точных целых — числитель над знаменателем, — сокращаемая при каждом действии; плюс, минус, умножить на, делить на и порядок перекрёстным умножением; записанный литерал проверяется на канон (пара, канонические половины, непустой знаменатель, сокращённость); ниже нуля и деление на нулевую дробь — отказы FLANG_PROPERTY своим словом; с число и точное целое не смешивается. Набор проб exact-fraction: 26 из 26, старое семя отвергает все 26.
• Остаток над точным целым (остаток от; задача 5245): шаг генератора glibc считается точно там, где double округляет произведение 1103515245·8388607.
• Предел потомку называет поручение, а не хозяин (ADR-0061): поручение «Запустить процесс с пределом» (память в КиБ, срок в мс) и отклик «Процесс оборван», который приносит напечатанное до обрыва. Два стенда — предел памяти и смерть узла — переписаны с оболочки на планы.
• Страница реестра пакетов печатается из ведомости и выкладывается на Pages (ADR-0059): реестр — ведомость имён, а не склад кода.
• check спрашивает судью планов: двенадцать подложных планов, которые раньше проходили проверку, теперь отвергаются.
• Экспериментальный каталог flang/experimental/: русская морфология для силлогизмов и демо, которое заполняет словарь и судит текст.
• У каждого приёма сверщика — теорема в Lean либо строка долга (ADR-0064; задача 4791). Список приёмов шаг_вывода снимается с checker.c прибором, а не пишется прозой: приёмов 83, в приёмке Lean 78, пять стоят строками долга с номером задачи. Н6 и О9, девять дней жившие без теоремы, вошли в приёмку; сторож lean-rules:check идёт на каждый пуш и краснеет в обе стороны, его три подлога — в CI. Побочно закрыта дыра: разбор случаев принимал ложное постусловие, подставляя условие текстом под связыватель; сверщик теперь отказывает.

Что изменилось

• Напечатанный Makefile называет заголовки каждого объекта (задача 7182): правка .h пересобирает зависящие объекты; до семени это доехало второй печатью подряд — печать Makefile принадлежит печатнику, а не исходникам.
• Семя перепечатано пять раз за двое суток, цена одной печати на gpu — 79–83 минуты (ведомость docs/reprint-ledger.tsv дополнена пятью строками); отпечаток входов печати называет коммит-источник семени.
• ADR «предел чужому процессу» получил номер 0061 — номер 0056 на стволе уже занят замерами кванторов; семь ссылок переехали.
• 122 добавленные строки длиннее 120 знаков укорочены без обхода сторожа роста: списки разборщика разорваны после запятых, куски таблиц лексера разнесены, примеры стендов и трёх сторожей переехали на функции-близнецы, описывающие ответ списком; значения примеров сняты прогоном.
• Отчёт С-2 сторожа ведомости правил называет число правил одной строкой, а разбивку по ADR — следующей; строка С-6 о бюджете checker.c короче на семь слов.
• Страница дорожной карты — датированный план до 1.0. Таблица помесячно с октября 2026 по апрель 2027, вехи 0.7.25, 0.8, 0.9 и 1.0, семь условий выпуска 1.0 и то, что решено не делать; прежний текст без дат снят.
• ADR-0067 о двоичных выпусках — предложено, кода нет. Выпуск будет нести готовые двоичные для четырёх троек с одним SHA256SUMS; пять задач (7959, 8128, 1710, 1504, 1098) и пять решений ждут владельца. Имена из решения, которых в исходниках нет, стоят в реестре «объявлено, не сделано».

Что сломалось

• Над двумя точными целыми отказ деления теперь перечисляет четыре действия, а не три: «плюс», «минус», «умножить на» и «остаток от». Пробы, ждавшие прежнее слово, пересняты.
• Дробь не входит ни в одну из десяти целей печати — эмиттеры её не знают; программа с точное дробное печатается только толкователем. Ключевого слова для целой части дроби нет; docs/flang/SPEC.md и DESCRIPTION.md не описывают ни точного целого, ни дробного — долг назван в ADR-0062 §6.

0.7.24 — 3 октября 2026

Линтер в языке, памятка ядра и три закрытые дыры в доказательствах

Что появилось

• flang lint — длина строки и глубина ветвлений, пределы из .flangrc. Ключи max-line-length и max-conditional-depth, поведение задаёт lint (refuse — отказывать). Заслон перед пушем судит только вашу правку: добавленная строка не длиннее предела, тронутая функция не глубже. Дерево пределам не отвечает, и ведомости долга нет по решению ADR-0053: flang lint по дереву находит 32 342 строки длиннее 120 знаков и 1365 функций глубже 2 — в 703 файлах из 1301 (снято 3 октября 2026). Правка этого выпуска убрала из своих строк 77 длинных, остальное осталось как было.
• Короткие команды живут в файле настроек. flang run-script <имя> берёт строку из .flangrc; ярлыки больше не прячутся в отдельном скрипте, и flang run-script без имени печатает, какие есть.
• Профиль библиотеки в .flangrc. Программа видит те модули стандартной библиотеки, которые назвал профиль, — замыкание меньше, а имена не сталкиваются.
• Памятка ядра: за один прогон чистый вызов считается один раз. Ускоряет проверку доказательств и печать семени; в напечатанном C памятка стоит обёрткой вокруг трёх функций ядра.
• Литерал-блок """ снимает общий отступ продолжений (ADR-0052). Длинный текст больше не обязан начинаться с нулевого столбца, и длинная строка в коде перестала быть выбором между пределом строки и правдой.
• В библиотеке появились длинное деление с остатком, НОД и точные рациональные. Деление и НОД стоят в bignum.flang — на 0.7.23 там не было ни того, ни другого; обязательств у него по-прежнему 9, новые функции постусловий не несут. rationals.flang — новый файл: дроби на длинных целых, 17 функций и 13 обязательств (сокращение, четыре действия, сравнение, гармоническая сумма). fmath.flang тоже новый, но это не функции, а четыре утверждения о неотрицательности длины и суммы; ни один файл дерева на них пока не ссылается.
• Доказательство словами: рассуждение пишется предложениями, посылки — допущениями (ADR-0050). Шаг называет правило ядра, а не номер строки.
• Сторож забытых времянок проверок. Неотслеживаемый каталог .flang-storozh-* или файл с «probe» в имени, оставшийся в дереве после снятого прогона, краснеет кодом 1 с путём; шесть мест, где времянка обязана лежать в дереве (компилятор ищет ввозимые модули относительно файла), сторож называет сам с причиной.
• Решение о точных целых записано, а отсутствие их держится пробой (ADR-0036, задача 1908). Числа в языке по-прежнему IEEE-754 double, и целые точны до 2⁵³−1. Набор flang/proof/probes/exact-integer/ каждым прогоном CI показывает, что точного целого в языке нет: литерал 42 остаётся числом, кольцевых правил для него у ядра нет. Проба покраснеет в тот день, когда появится, — и это её работа.

Что изменилось

• Независимая проверяющая программа переигрывает больше. Шаги «по предположению» из посылок утверждения, шаги по свойству, ссылки между файлами, проекции полей, типы модулей и наборы зависимостей — как их видит сборщик, — и то, что ядро доказывает в ваших программах, а не только в дереве языка.
• Тождество над открытым термом больше не объявляется ложью (4850). Ход «подставить терм вместо самого себя» принимается без вычисления, а терм, который нельзя вычислить, уходит в «не взялся» (код 3), а не в расхождение (код 1): место, которого прогон не взялся проверять, — не ложь.
• У независимого сверщика появился ключ --строго. Он спрашивает не «не противоречит ли запись исходнику», а «доказано ли САМО»: обязательство должно быть хотя бы одно И каждое числиться доказанным, иначе исход 3 с названной причиной. На девяти программах набора строгих проб шесть ответов «ноль» стали «три» — включая запись к программе с ложным постусловием, которой прежде ноль давали все три прибора.
• Запись доказательства, отставшая от исходника, отвергается, а сама проверяющая программа пересобирается, если её исходник новее двоичного: старый двоичный больше не судит новый исходник молча.
• Вердикт дерева — ДОКАЗУЕМ, и набор проб под ним вырос. Доля, переигранная независимым проверяющим, стоит на 100,00 % — 650 обязательств из 650; порог вердикта ровно 100 %, и он взят. Против 0.7.23 выросло не число доли, а набор, которым она держится: подделок в манифесте 36 → 38, проб на подлог 575 → 631, честных проб 274 → 315, вынесенных недостижимых мест 27 → 30, и храповик набора поднят вместе с ними. Четыре проверки вердикта: калькулятор из проверяющей программы снят, доля не ниже порога, набор проб пройден, набор не ослаб. Снято io scripts/provability.fscript --plan Verdict: по 0.7.23 — прогон CI 29 сентября 2026 на main, по 0.7.24 — прогон 3 октября 2026 на ветке выпуска.
• Оснастка переехала с shell и Python на планы flang. Сторожа, пробы и приборы счёта теперь планы; заслон перед пушем запрещает рост shell, Python и лишнего markdown, а CI судит сообщение коммита по уговору (префикс, длина заголовка, только ASCII).
• Справочник и сайт переписаны простыми словами. README говорит, что язык делает и как его поставить; docs/DESCRIPTION.md больше не привязан к выпуску («описание соответствует 0.7.23» убрано) и не печатает числа, меняющиеся от сборки к сборке. Датированных отчётов в дереве больше нет — кроме двух в docs/archive/, на которые ссылается ROADMAP; из docs/ за выпуск ушло 418 файлов.
• Дата из числа дней верна ниже года один. Поправка, написанная для усечения, срабатывала второй раз под делением-полом, и день −719834 давал −719833. Круг «дни → дата → дни» сходится теперь на 1038 днях подряд у границы эры, на 7240 днях шагом 1009 и на 4000 псевдослучайных — расхождений 0.
• Отпечаток семени находит свой коммит по содержимому. Прежде он называл sha, умиравший при переносе ветки, и быстрая сверка отказывала словами «коммит дереву неизвестен»: четыре из пяти значений за двое суток были мертвы. Теперь на красном пути прибор ищет самый молодой свод, чьи входы печати сходятся с отпечатком файл в файл, и правит одну строку ключом --perekommit.
• Проводник flangtutor принимает верные ответы. Значение урока читается из stdout, а не вместе с потоком ошибок, куда идёт вердикт доказанности; список слов языка в проводнике догнал таблицу лексера (649 фраз против 647), и проба проводника зелена целиком.
• Кириллических путей в дереве 5 вместо 67 (вне flang/proof — 4 вместо 66). Остаток назван в ведомости с доводом: четыре файла в flang/test называет сам flang/self, и имена уезжают в семя дословно, а letters.фп — проба расширения. Транслитные имена из flang/self тоже ушли: пять файлов (zapis.flang → proof-record.flang и ещё четыре) названы по-английски. Сторож отвечает «кириллица в путях: 5, все в ведомости — новых нет», код 0.

$ flang run-script cyrillic:check
кириллица в путях: 5, все в ведомости — новых нет                 код 0

• Заслоны роста судят правку, а не состояние дерева. Переименование файла больше не выглядит для них новым файлом: git --numstat отдаёт слитый путь docs/{прежний => новый}, и заслоны приводят его к новому пути. Порог схожести — 50 % (поправка к ADR-0053).
• Сторож кириллицы смотрит весь путь, а не последнее звено. Латинское имя файла в кириллическом каталоге прежде проходило молча; теперь приговор называет путь целиком.
• flangtutor выбирает локаль и awk прогоном. На машине, где /usr/bin/awk — это mawk, урок приходил мусором: mawk режет закрывающую «»» по байту. Теперь пара «локаль + awk» проверяется на целость UTF-8, а годной пары нет — краска снимается, и текст остаётся целым.
• Заслоны перестали врать молчанием. Заслон перед пушем обрывал проверку, молчащую дольше 200 с, и отвечал «проверки не запущены»: на выпускном диапазоне так не прогонялась ни одна из его 21 проверки (lint:growth молчит ~290 с). Предел молчания теперь 900 с. Сам заслон длинных строк просил у git весь дифф и упирался в предел вывода 1 МиБ на напечатанном семени из 685 001 строки — теперь он просит только те пять расширений, которые линтер умеет читать, и это проверено отрицательным контролем: без приставки :(top) путь не совпадает ни с чем и заслон зеленел бы молча.

Что сломалось

• Теорема, гипотезы которой нет у утверждения, отвергается (5311). Раньше такая теорема доказывала утверждение слабее объявленного; программы, где это проходило, станут красными — и правильно.
• Завершаемость видит вызов через функцию-значение (3870). Функция, которая считалась тотальной только потому, что вызов шёл через значение, тотальной больше не считается.
• Постусловие с таких что цитируется только после снятия ограничения (4573): ссылка на него до снятия больше не принимается.
• Три кода отказа и указатель заметок получили английские имена. Кто сверялся со старыми строками кодов — поправить сверку.
• Приборы на shell и Python убраны (scripts/target-census.sh, Python-приборы доли доказанного). То же считают планы flang; старые пути вызова не работают.
• Пуш встаёт на линтере, если добавленная строка длиннее предела или тронутая функция глубже: пределы берутся из .flangrc дерева, а не из привычки.
• flang test отвечает кодом 3, когда блоки «прогон» не исполнены. Прежде файл с блоками прогон давал код 0 и слова «примеров 2, прошло 2» — заведомо ложное ожидание в блоке проходило молча. Теперь рядом со счётом примеров стоит строка «блоков «прогон» N, исполнено 0», а исход — «сделано, но проверено не всё». Сборочный сценарий, читавший ноль, станет красным, и правильно: блоки по-прежнему не исполняются (планировщик вне замыкания двоичного, задача 1104).
• 153 коротких команды живут в .flangrc и носят английские имена. В 0.7.23 ярлыков в файле настроек не было ни одного. Кто звал прежние русские имена, зовёт теперь английские: подсчёты:проверка → counts:check, тесты → tests, столкновения:проверка → link-collisions:check.

0.7.23 — 29 сентября 2026

Поле записи проверяется по своему типу, и прогон знает предел памяти

Что появилось

• --memory-limit N (--предел-памяти) — предел памяти прогона. Годится при любой команде. У check, test и run по умолчанию три четверти памяти машины; 0 снимает предел. На пределе прогон останавливается кодом 5 и называет функцию, которая считалась.

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

Заявка #160.

• Шаг доказательства называет правило ядра. Строка шага в записи --record кончается словами правило «…», в --proof --json есть поле stepRules. Независимая проверяющая программа сверяет имя с правилом, которое применяет сама.

$ flang check chain.flang --proof --json
… "stepRules":[{"step":1,"line":33,"rule":"цель есть допущение"}, …]

Что изменилось

• Поле записи проверяется по объявленному типу. Поле неотрицательное принимало -7, и ядро доказывало обещание, которое прогон потом нарушал. Теперь такая программа не проходит проверку типов.

объект «Мера»
  «шаг»: неотрицательное

тотальная функция «Отрицательный шаг»
  возвращает неотрицательное
  обеспечивает «итог не меньше нуля» результат не меньше 0
  (запись «Мера» с «шаг» равным -7).«шаг»

0.7.22: $ flang check step.flang
step.flang: проверено — разбор, типы, завершаемость, ядро и примеры; замечаний нет   код 0

0.7.23: $ flang check step.flang --proof
FLANG_TYPE в файле step.flang, строка 9, столбец 33: поле «шаг» записи «Мера»: ожидался неотрицательное, получен целое   код 1

• flang io: истёкший срок процесса — «Сбой» FLANG_IO_TIMEOUT. Раньше хозяин отвечал «Процесс убит» SIG9, как при убийстве снаружи. --timeout — срок тишины, отсчёт от последнего байта вывода, по умолчанию 30000 мс; ключ теперь есть в flang io --help.

$ flang io child.fscript --timeout 1000 -- 'sleep 3'
… "failed FLANG_IO_TIMEOUT: программа «sh» молчала дольше 1000 мс и оборвана хозяином (--timeout)"

Заявка #162.

• Интерпретатор освобождает память на глубокой рекурсии. На рекурсии глубже примерно 500 вызовов память не освобождалась и росла с каждым шагом. «Числа до» от 1000 раньше упирался в 3,6 ГБ, теперь идёт в 370 МБ.

Заявка #160.

• разделить … по и содержит в C-рантайме ищут разделитель через memchr. На 100 МБ текста разделить — 0,47 → 0,08 с, содержит — 0,39 → 0,008 с; число шагов то же.

Заявка #161.

• Ключи .flangrc — по-английски. language, surface, color, page, version, name, license, repository, issues, unproven. Старые ключи пока читаются и называют замену.

$ cat .flangrc
недоказанное = разрешение
$ flang run p.flang --function «Ответ»
flang: .flangrc: запись «недоказанное = разрешение» устарела и пока читается — замените её на «unproven = allow»
42

• Строковые литералы в записи доказательства печатаются как есть. Раньше пробелы расставлялись и внутри строк: вместо "://" стояло " : //".

Что сломалось

• Поиск модуля по имени не выходит выше корня проекта. Корень — ближайший каталог с .flangrc, .git или flang.package. Файл выше корня больше не подменяет модуль проекта или библиотеки; модуль, лежащий только там, не находится.

$ flang check app/main.flang
FLANG_IMPORT_NOT_FOUND в файле app/main.flang, строка 1, столбец 1: не найден модуль «Мера»   код 1

Миграция: перенесите модуль в дерево проекта, ввезите его путём (использует «Мера» из "../mera.flang") или назовите предел поиска переменной FLANG_MODULE_ROOT.

0.7.22 — 26 сентября 2026

Силлогизм следует и верный код символа вне базовой плоскости

Что появилось

• следует — вывод утверждения из посылок, названных выше. Заключение записывается отдельным блоком и ссылается на доказанное утверждение словом по свойству.

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

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

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

Без строки по свойству заключение не доказывается:

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

Что изменилось

• код символа в оболочке: знаки вне базовой плоскости. flang repl отдавал 240 — первый октет UTF-8 — на любом таком знаке; flang run на том же выражении отвечал верно. Теперь ответ один.

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

Заявка #103.

• Ключа --step-limit у самого двоичного нет. Ранняя редакция этих заметок обещала, что ключ годится при любой команде. В 0.7.22 его разбирает только flang check.

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

Что сломалось

• Скрипты печати семени переименованы. Касается тех, кто пересобирает компилятор из исходников.

Миграция: замените имена в своих скриптах и в настройке CI.

0.7.21 — 22 сентября 2026

Недоказанный код больше не запускается по умолчанию

Что появилось

• Переменные окружения и доводы командной строки в планах. Поручения были в словаре языка, а рантайм отвечал на них FLANG_IO_UNKNOWN.

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

Ответ — «Значение среды» с полем значение, либо «Переменной среды нет» отдельным вариантом, а не пустой строкой. Доводы плана — всё, что стоит после --:

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

Запретить: --no-env, --no-args.

• Вывод на терминал. «Показать» кладёт кадр, «Ждать событие» ждёт клавишу:

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

Клавиша приходит как «Случилось» с полями откуда и значение; по сроку — «Срок вышел». Имена клавиш: ввод, пробел, таб, возврат, выход, вверх, вниз, влево, вправо; печатный знак приходит собой.

Рабочий пример — docs/examples/io/progress-bar-on-screen.flang. Кадр идёт на /dev/tty, а не в stdout: там итог плана в JSON. Нет терминала (труба, файл, CI) — ответ прежний, FLANG_IO_NO_SCREEN. Ctrl-C по-прежнему убивает программу. Запретить: --no-screen.

• bootstrap/flang io scripts/four-coverages.fscript --plan Measure --timeout 900000 печатает четыре покрытия порознь, у каждого своя строка «чего это не значит», и рядом с числом стоят дата и коммит.

Что изменилось

• Независимый сверщик перестал принимать ложное доказательство. Две дыры: подстановка доводов шла последовательно вместо одновременной, подстановка тела не спрашивала захват имени. Ни 529 мутационных проб, ни четыре проверки дерева их не ловили.
• Он же перестал отвергать честные записи — вердикт зависел от порядка, в котором напечатаны блоки.
• Доля мест, которые сверщик переигрывает независимо, — 650 из 650. Мест, где он верил ядру на слово, не осталось; прежде их было 12 посылок и 4 шага.

Что сломалось

• flang run и flang io выходят кодом 3, если обещание функции не доказано. Раньше такая программа запускалась и отвечала кодом 0.

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

Миграция: добавьте --trust — вердикт не будет считаться вовсе.

Затронуты сценарии, звавшие flang run или flang io на программах, где обеспечивает закрыто только примерами. Проверить заранее: flang check --proof <файл> — итог «доказано 0, сетка N» значит, что программа попадёт под новое правило.

0.7.20 — 18 сентября 2026

Компилятор доказан сам себе целиком: 650 мест из 650 переиграны независимой программой

Что появилось

• Впервые вердикт bootstrap/flang io scripts/provability.fscript --plan Verdict --timeout 900000 говорит ДОКАЗУЕМ при пороге 100 %: каждое из 650 обязательств в записях собственного доказательства компилятора независимая программа на C переиграла сама, не приняв от компилятора ни одного шага на слово. Раньше часть мест она брала на веру, и порог был ниже.
• Снятие предусловия (требует) на месте вызова теперь печатается в запись и переигрывается: вторая доля, которая считает и предусловия, тоже 652 из 652.
• Перепечатка семени привезла в собранный компилятор правки ядра: предусловие вызова не снимается объявленным типом довода; в требует можно писать квантор по элементам списка; у выписанного списка, отобразить и применённого ярлыка появились права; ядро печатает в запись обоснование, которое раньше выбрасывало.

Что изменилось

• Порог доказуемости поднят с 95 % до 100 % — слово владельца. До перепечатки вердикт при этом пороге честно печатал НЕ ДОКАЗУЕМ.
• package.json выброшен из дерева: настройки проекта читаются из .flangrc, а сторож не даёт файлу вернуться.
• Правила вывода снова сверены чужим ядром — Lean 4.34.0: строк ведомости 109, лемма есть у 107, на 1488 проигранных выводах сверщик и Lean разошлись 0 раз.

Что сломалось

• Доказательство по-прежнему относится к исходнику, а не к напечатанному коду: что flang emit --target c напечатал именно проверенную программу, не проверяет никто. Тот же разрыв у Coq, Lean и Idris.
• Сверщик — сам доверенный код: 7531 строка кода на C при потолке храповика 7603, правила сверены Lean, но доказан он не был.
• О состоянии во времени, побочных эффектах и параллелизме правил всё ещё нет: мест, которым они нужны, 414, и первые три шага только расписаны.
• 100 % — это доля мест в собственном доказательстве компилятора, а не «все программы доказаны». Вердикт о вашей программе даёт flang check --proof и сверщик рядом с ней.

0.7.19 — 13 сентября 2026

Кванторы дошли до собранного компилятора

Что появилось

• Теперь можно сказать «для всех элементов этого списка» — и компилятор это докажет. Раньше квантор связывал только простые имена, а про элементы списка сказать было нечем. Работают и вложенные кванторы: «для каждого элемента и для каждого другого элемента».
• Индукция по вашему собственному объявленному типу. Раньше доказать что-то про свой тип разбором случаев было нельзя — правила знали только встроенные типы.
• Утверждение можно писать не при функции, а само по себе: «утверждение «длина любого списка неотрицательна»». Такие утверждения теперь доходят и до машинного отчёта, и до описи доказанного.
• Шаг доказательства можно назвать словами: шаг теоремы называет правило и посылки, а ядро проверяет, что названное сходится. Раньше шаги были безымянными.
• Компилятор печатает в TypeScript, и справка наконец об этом говорит. Печать работала и раньше, но flang --help о десятой цели молчал: семя отстало от исходников одной строкой.

Что изменилось

• Правил вывода в ядре стало тринадцать вместо двенадцати — добавилось правило для существования со свидетелем. Теорем в дереве языка 284.
• Установка через Homebrew проверяется целиком. Пять поломок найдено и починено: справка называла девять целей печати при десяти рантаймах в поставке; сообщения об ошибке падали сами на старых оболочках Apple; проверка версии требовала ответа одной строкой, а он нарочно двухстрочный; подсчёт каталогов не ходил по ссылкам, а Homebrew кладёт именно ссылки.
• Английская страница выпусков звала журналы уровнем выше корня сайта — четыре ссылки вели в никуда.
• Правка задачника больше не пересобирает компилятор в облаке: две работы ходили на каждый пуш без разбора.

Что сломалось

• Доля независимой проверки не выросла: 629 обязательств из 651, те же 96,62 %. Перепечатка семени дала новые умения ядра, а не прирост доли. Мест, где проверка верит компилятору на слово, по-прежнему 12 посылок и 4 шага.
• Верить приходится большему, чем вчера: решающая часть ядра выросла с 4669 строк до 4796. Кванторы живут именно там, вынести их некуда. Наряд снизить это число ниже 4000 остаётся невыполненным.
• О состоянии во времени, побочных эффектах и параллелизме логика по-прежнему не знает ничего. Работа над этими тремя вещами начата, но в этот выпуск не вошла.
• Доказательство относится к flang check и не покрывает собранный код: никто не проверяет, что напечатанный C соответствует исходной программе. Тот же разрыв есть у Coq, Lean и Idris.

0.7.18 — 12 сентября 2026

Проверка стала строже, а дерево — понятнее

Что появилось

• Независимая проверка теперь повторяет 629 обязательств из 651 вместо 625 — это 96,62 %. Мест, где она верит компилятору на слово, стало 12 вместо 16. Прибавка получена повторением шагов, а не вычислением: разряд «закрыто вычислением» остался прежним, 6.
• Учебник в терминале вырос с пяти уроков до двенадцати. Он больше не просит набрать программу целиком: даёт готовый текст с пропусками и спрашивает их по очереди, а после каждой строки говорит, что понял. Имя можно писать и ёлочками «Удвоить», и прямыми кавычками — компилятор принимает оба вида, и учебник больше не спорит об этом.
• Проверка обязательств у свободного утверждения (того, что стоит не при функции) теперь доходит до машинного отчёта flang check --proof --json. Раньше такие утверждения выпадали из отчёта в трёх местах отбора, и их не видели ни опись доказанного, ни числа на сайте.

Что изменилось

• Примеры программ переехали из examples/ в docs/examples/: 200 программ в 24 каталогах. Рабочие скрипты разложены по восьми папкам — у корня каталога scripts/ осталось 13 файлов вместо 136. Замеры, которые давно не гонялись, сняты; живые переехали в docs/benchmarks/ с английскими именами.
• Браузерные образцы (web/) стали тем, чем они и были, — примерами: теперь они лежат в docs/examples/web/.
• Файл package.json оставлен, но вычищен: из него сняты три поля, которых не читает ни один инструмент. Он нужен не для npm, а как единственное место, откуда выпуск, два сторожа, формула Homebrew и сборка сайта берут версию, лицензию и адреса.
• Сторож имён поймал настоящее столкновение: тип «Документ» объявлен и в разборе JSON, и в языковом сервере, а зонд проверки сводил оба в одну программу. Починен не сторож, а причина — из зонда снят ввоз, которым он не пользовался.

Что сломалось

• Кванторы по элементам списка, вложенные кванторы, индукция по вашему собственному типу, утверждения не при функции и шаги доказательства, названные человеком, в этот выпуск НЕ вошли. Они сделаны и проверены, но доходят до собранного компилятора только перепечаткой семени — она идёт и займёт ещё несколько часов. Выйдут следующим выпуском.
• Доказательство по-прежнему относится к flang check и не покрывает собранный код: никто не проверяет, что напечатанный C соответствует исходной программе. Тот же разрыв есть у Coq, Lean и Idris.
• Опись примеров (ведомость-примеров.txt) держит прежние пути: обходчик, который её печатает, идёт два часа сорок минут и ни разу не дошёл до конца — ни у нас, ни в конвейере. Переписать её руками нельзя: сверка идёт построчным сличением, а порядок строк там — порядок обхода.

0.7.17 — 11 сентября 2026

Язык прошёл собственную проверку на доказуемость

Что появилось

• Команда ./ярлык доказуемость впервые отвечает ДОКАЗУЕМ. Как это работает: когда компилятор проверяет программу, он записывает, какое утверждение доказано и какими шагами. Отдельная программа на C, написанная без оглядки на компилятор, берёт исходник и эту запись и повторяет каждый шаг сама. Повторено 625 обязательств из 651 — 96 %.
• Проверка «проверяющая программа не считает сама вместо повторения шагов» теперь не ищет имя функции в коде, а запускает настоящую пару исходник + запись, в которой есть цели, доказуемые только переписыванием. Честная программа за такие цели не берётся. Под этой проверкой 34 вида обязательства.
• Подложных записей стало 401. Каждая лжёт по-своему: подменяет тело функции, ссылается на запрет вместо правила, выдаёт вычитание за сложение, ставит номер строки мимо объявления. Ни одна не принята. Мы не говорим, что проверяющая программа правильная, — мы показываем 401 попытку её обмануть.
• 88 правил вывода проверены второй, независимой системой — Lean 4. Рядом с каждой леммой лежит наша строка правила дословно, чтобы человек мог сверить глазами. Восемь нарочно испорченных правил Lean отверг все восемь.
• flangtutor — учебник в терминале в духе vimtutor — теперь входит в поставку. Пять уроков, ответ проверяет настоящий компилятор. Ставится вместе с flang через Homebrew и asdf.
• Проверка свежести записей отличает запись, испорченную нарочно, от записи, отставшей от компилятора, и отказывается мерить устаревшим двоичным файлом.

Что изменилось

• Доля обязательств, повторённых независимой программой: 79,88 % → 96,01 %. Прибавка получена повторением шагов, а не вычислением: мест, закрытых вычислением, стало меньше — 8 → 6.
• Lean нашёл у нас неверное правило, и оно починено. Правило о прибавлении одного и того же к обеим сторонам неравенства требовало, чтобы прибавляемое было «ограничено», а это слово допускало и ограниченность только сверху — то есть минус бесконечность. Рабочее правило от ложного отличалось одним словом.
• Тип нат называется неотрицательное. Старое имя остаётся синонимом до 1.0.
• flang package снова работает. Он был сломан на любом входе с 29 августа: функция о двух аргументах вызывалась с одним.

Что сломалось

• Доказательство относится к flang check и НЕ покрывает собранный код: никто не проверяет, что напечатанный C соответствует исходной программе. Тот же разрыв есть у Coq, Lean и Idris. Как его закрывать — в решении ADR-0030: проверять каждый запуск печатника, а не печатник целиком.
• Что логика умеет и чего нет, измерено запуском. «Итог не меньше стоимости товаров» при сложении — доказано. «Скидка не делает цену отрицательной» при вычитании с предусловием — объявлено, не доказано. О состоянии во времени, побочных эффектах и параллелизме логика не знает ничего.
• Писать на flang программы для медицины, авиации и космоса нельзя. Там требуется сертификация процесса: след от требования к коду и тесту, квалифицированные инструменты, доказанные границы времени отклика, поведение при отказе оборудования. Ничего из этого у нас нет, и проценты это не заменяют. Разбор — в решении ADR-0031.
• Архив выпуска не совпадает побайтно между сборкой на своей машине и сборкой в конвейере GitHub, хотя собирается нарочно повторимым способом.

0.7.16 — 9 сентября 2026

Чекер переигрывает вывод факта о типе; дорога до конца измерена поимённо

Что появилось

• ПРИЁМ «ВЫВОД»: независимый чекер переигрывает записанный вывод факта о типе — шаг за шагом, а не по имени правила. Заключение каждого шага записано формулой языка и сличается знак в знак; цель блока сверяется С ИСХОДНИКОМ, а не берётся из записи; каждое основание проверяется по существу (строка обязана быть объявлением довода, допущением либо телом той функции, о которой речь); имена, помеченные в списке правил как запрет, отвергаются. Решение ADR-0022: факт о типе едет в записи ВЫВОДОМ, а не аксиомой и не именем правила.
• Проб на подлог стало 219 вместо 200: девятнадцать новых ловят ложь именно в блоке вывода — чужая цель, номер мимо объявления, пропущенная посылка, не та посылка, переставленный шаг, развёртка не на тело, оборванный вывод, имя вне списка правил, подмена вычитания суммой, ссылка на запрет вместо правила. Ни одна подделка не принята, ни одна честная запись не отвергнута.
• flangtutor — проводник по языку, как vimtutor: пять уроков по нарастанию, от модуля и функции до постусловия и отчёта о доказательстве. Ответ человека судит НАСТОЯЩИЙ компилятор — разбор, типы, завершаемость, примеры, — а не сличение строк. Место в уроках запоминается, работа продолжается с прерванного. Язык берётся из файла настроек.
• Ctrl+L в оболочке очищает экран и возвращает набранное на место. Клавиша работала и раньше, но не была закреплена ни одной проверкой — теперь закреплена обеими половинами.
• flang package снова работает. Он был сломан на любом входе с 29 августа: ведомость звалась одним доводом при функции о двух. Проверено сквозным прогоном: flang new создаёт пакет, flang package его собирает, пакет ввозится.
• FLANG_MODULE_ROOT обрывает поиск модуля выше названного корня. До этого поиск поднимался ВЫШЕ корня дерева, и файл-предок каталогом выше побивал библиотеку языка — шесть живых мест, ни одной проверкой не пойманных.
• Тип нат называется неотрицательное. Сокращение не читалось; старое имя остаётся синонимом до 1.0.

Что изменилось

• Доля корпуса, проверенная независимым чекером: 517 / 651 = 79,42 % → 520 / 651 = 79,88 %. Прибавка от двух новых печатников; знаменатель не двигался.
• Печать в Elixir перестала лить мёртвую строку результата на каждое постусловие — семнадцать предупреждений в одном файле ушли в ноль.
• Внутренние слова проекта убраны из страниц для читателя: тринадцать мест переписаны словами, «проверка» вместо «сторож», «отчёт» вместо «ведомости». Две строки оставлены — это дословная цитата вывода компилятора, и переписать её значило бы соврать о том, что читатель увидит у себя.
• Битых ссылок в дереве 1947 → 18. Проверка научена отличать запись о прошлом (сделанную задачу, датированный отчёт) от обещания о настоящем и печатает число пропущенного, а не прячет его.
• Список правил вывода вырос до 71 строки в двух записях, логической и категорной, сверенных с кодом ядра построчно.

Что сломалось

• Вердикт по-прежнему НЕ ДОКАЗУЕМ: три проверки из четырёх сошлись, доля 79,88 % при пороге 95 %.
• Дорога до конца измерена поимённо: недостижимых мест НЕТ НИ ОДНОГО, потолок работы 643 / 651 = 98,77 %. Последние восемь мест — не работа, а решение о том, что именно обещает число.
• Найдено при выпуске и не скрыто: релизный архив не совпадает побайтно между сборкой на своей машине и сборкой в конвейере, хотя собирается нарочно повторимым способом. Обещание «соберите сами и сверьте» сегодня не выполняется.

0.7.15 — 8 сентября 2026

Калькулятор снят из чекера: гейт независимой проверки закрыт

Что появилось

• ГЕЙТ Г7 ЗАКРЫТ. Из чекера убран ход, который ДОКАЗЫВАЛ утверждение, вычисляя его, вместо того чтобы проигрывать записанные шаги. Убран в обеих точках: сняв его в одной, работу немедленно подхватывала вторая (дверь половина_закрыта, тождественны на глубине 6), и проверка грепом по имени печатала при этом ноль. Сторож подлога отделён от вычислителя и остался на месте. Тождество знак в знак и замкнутый счёт сохранены.
• Проверка гейта на калькулятор больше НЕ ГРЕП ПО ИМЕНИ, а прогон по живой паре исходник+запись (flang/proof/checker/tests/records/identity-after-rewrite/p1-goal-not-an-equality). Две ∀-цели там доказуемы только переписыванием тела законами, ходов в записи нет ни одного — честный чекер обязан оставить их на слове ядра и назвать поимённо. Ловушка ДВУСТОРОННЯЯ: третья цель закрывается тождеством знак в знак и обязана остаться закрытой, иначе проверку брал бы и чекер, сломанный до состояния «ничего не доказываю». Переименование функции обойти проверку больше не может.
• Прибор доказуемости bootstrap/flang io scripts/provability.fscript --plan Verdict --timeout 900000 гоняет ЧЕТЫРЕ проверки и печатает все четыре числами, каким бы ни был исход предыдущих. Прежде он замыкался накоротко: провалилась первая — остальные не гонялись вовсе. Сторож, который не гоняется, не сторож.
• Манифест набора подделок flang/proof/forgeries/manifest.tsv — 31 строка, класс каждой подтверждён чтением шапки исходника. Храповик ratchet.txt держит два числа: сколько подделок объявлено и сколько мест их честных половин проиграно. Проверка 4 краснеет, если набор ослаб. Одна подделка при сверке оказалась не того класса, каким числилась.
• Ведомость правил вывода flang/proof/tables/inference-rules.tsv — 71 строка в ДВУХ нотациях, логической и категорной, сверенная с кодом ядра построчно. Согласие нотаций проверяемо, а не декларативно: каждая посылка пронумерована, и категорная запись обязана назвать её место. Четыре сторожа с восемью пробами на подлог. Решение ADR-0022: факт о типе едет в записи выводом, а не именем правила и не аксиомой.
• Файл настроек .flangrc и выбор языка вывода (решение ADR-0024). Пары «ключ = значение», не JSON и не программа: файл читается до того, как язык готов говорить. Старшинство: довод, среда, файл проекта, файл дома, локаль, умолчание. Подъём обрывается на первой примете, поэтому дальний файл не перекрывает ближний.
• Оболочка печатает отпечаток своей сборки второй строкой flang --version: восемь знаков sha256 самого исходника оболочки. Взято у iex: дополнение по Tab, .очистить, история между запусками файлом, вставка без мельтешения (замер на одной вставке: 90 перерисовок было, 10 стало).
• Десятая цель печати — TypeScript. Оба README и сторож обещаний печати считают десять.

Что изменилось

• Знаменатель доли СУЖЕН решением ADR-0023: из него вынесены места, недостижимые в принципе — обязательства записи, которую чекер отвергает целиком. Вынос идёт по ДВУМ признакам сразу, объявлению манифестом И измеренному отказу чекера: по одному замеру порча записи растила бы долю. Доля 517 / 651 = 79,42 % против 517 / 665 = 77,74 % прежней меры. Числитель не изменился ни на место, баланс печатается и сверяется.
• Комментарии сняты из 58 файлов на flang, минус 7429 строк. Код каждого файла сверен без комментариев байт-в-байт, вывод flang check и flang test --ledger — знак в знак до и после.
• Битых ссылок в дереве 1947 → 18. Сторож научен отличать запись о прошлом (сделанная задача, датированный отчёт) от обещания о настоящем, и число пропущенного печатает в вердикте, а не прячет. Список исключений при этом не раздут, а сокращён: 373 строки → 171.
• Тело выпуска на GitHub печатается из docs/release-notes.json, а не из строки в конвейере. У 0.7.14 на 93 коммита приходилось 168 знаков тела. Выпуск без записанных заметок теперь отвергается.
• .claude и AGENTS.md переехали в .ai/, README.ru.md — в docs/. Корень отделяет язык от оснастки.
• Версия больше не живёт в package.json: он печатается из scripts/release/emit-package.flang.

Что сломалось

• Доля с прежними выпусками несравнима второй раз подряд: 0.7.14 сменил числитель, 0.7.15 сужает знаменатель. Обе меры печатаются с разбивкой, и баланс знаменателя сверяется прибором.
• flang package не работает ни на одном входе с 29 августа: вызов с одним доводом при функции о двух. Найдено прогоном, починка — одна строка, доедет следующей перепечаткой семени (задача 3401).
• Поиск модулей поднимается выше корня дерева, и файл-предок каталогом выше побивает библиотеку языка. Дыра названа и померена: 20 имён затеняемы, 5 затенений живых. Сторож scripts/guards/module-origin-guard.sh её видит, починка в двоичном ждёт перепечатки (задача 3127).
• Вердикт по-прежнему НЕ ДОКАЗУЕМ: три проверки из четырёх сошлись, доля 79,42 % при пороге 95 %.

0.7.14 — 7 сентября 2026

Чекер сам проигрывает доказательства завершения

Что появилось

• Сертификат тотальности КОМПОЗИЦИИ. Двоичный печатает в запись доказательства свидетельство «функция завершается, потому что рекурсии в ней нет — только вызовы уже завершённых», а независимый чекер проигрывает это свидетельство заново (сверить_тотальность), а не верит имени правила. Переигрыш не зависит от порядка блоков в записи: два прохода и обнаружение цикла. Семя перепечатано, 82 записи корпуса напечатаны заново. Коммиты ff1dc5b7, cbac34ce, 7cd56073, fba02c9a.
• Сертификат тотальности РЕКУРСИИ, виды structure и step: завершение по спуску вдоль варианта индуктивного типа и по убывающей мере, не меньшей нуля. Двоичный печатает узел с полным свидетелем — убывающий довод, дно, витки, самовызов, — чекер его проигрывает. Честно: на нынешнем корпусе прирост доли около нуля, потому что корпус доказывает завершение рекурсии над встроенным списком типовым законом, а не этими сертификатами; способность влита как задел. Коммиты 4bfbd217, 5d73d391, d1bbbf94.
• Прибор доли-проигрыванием: sh flang/proof/corpus-share.sh --проигрыванием. Числитель — обязательства, которые чекер действительно проиграл заново; знаменатель — ВСЕ обязательства корпуса, включая снятые на слово ядра и обязательства отвергнутых записей. Ни одна запись из знаменателя не выпадает. Коммиты 00a56ba5, 682006f5.
• Межмодульная линковка сертификата тотальности (--набор, --зависимость): доверие набору записей берётся только по проигранному носителю. На нынешнем корпусе таких мест ноль — вписано впрок, а не по нужде. Коммит 4743a313.

Что изменилось

• Линейка доли считает по-новому, и число с прежними выпусками несравнимо: шаги «по примеру» и «по свойству», которые чекер и так проверяет вычислением, попадают теперь в числитель, а не только в знаменатель. После сертификата тотальности композиции доля 47,33 %, после кредита за проверенное по существу — 60,78 %; доверенная база при этом не растёт и перепечатка не нужна. Печать доли даёт разбивку: ходами и по существу. Коммит f5ca9e8f.
• Теория категорий переехала: каталог flang/cat стал flang/ct, проза — docs/ct. Коммиты acca80a3, 8142524b.
• Из 192 файлов примеров убраны //-комментарии и дубли, а http.flang переписан таблицей данных вместо 55 однотипных записей. Коммиты bfd86834, 853d2f01, d2779328.

Что сломалось

• Язык по-прежнему НЕ формально доказуемый. В чекере остаётся запасной калькулятор перепиской: часть целей он пересчитывает, а не проигрывает записанные ходы. Пока он на месте, ярлык доказуемость отвечает НЕ ДОКАЗУЕМ, и снять калькулятор частично нельзя — доля обрушится целиком.
• Порог 95 % на этом корпусе не гарантирован даже в пределе: подделки корпуса нарочно держатся в знаменателе (иначе долю можно было бы накрутить), а в числитель попасть не могут, поэтому структурный потолок лежит примерно между 91 % и 96 % — порог внутри этой вилки.

0.7.13 — 6 сентября 2026

Объект доказательства: чекер проверяет готовый вывод ядра, а не пересчитывает его

Что появилось

• Двоичный сам печатает переигрываемый след доказательства для пяти семей тождества — соседи, рефлексивность, длина, элемент, вычислить. До сих пор цепочку ходов умел строить только чекер. Первый сквозной прогон зелёный: двоичный издаёт след, независимый сверщик проигрывает его, «на слово ядра 0». Семя перепечатано. Коммиты 2eb5633e, c3d17187.
• Приём «постусловие вызванной»: чекер сам строит инстанцию постусловия по вызову — арность, подстановка параметров аргументами и результата узлом — и закрывает цель модус-поненсом, вместо прежней привязки «имя плюс строка». Приём ловит настоящую подделку: теорема с целью «результат равен 3» при теле, дающем 0, раньше проходила кодом 0, теперь даёт код 1. Коммиты e5a75366, d433f3b2.
• Ходы «вычислить» (замкнутый счёт вида «2 плюс 2 равно 4») и «переписать формой» (законы длины и элемента) проигрываются явными примитивами поверх оценить_терм, а не принимаются на слово ядра. Коммиты a1f19f27, 269d3ccf, b0ef3a31.
• хеш256 стал встроенным словом языка: SHA-256 считает рантайм каждой из девяти целей печати, а не библиотека на flang. Коммиты 5c90d6f7, ee3b0121.
• У цели js появился хозяин на Node — flang/src/emit/js/flang_host_node.js. Программа с планом ввода-вывода, напечатанная в JavaScript, теперь исполняется: девять родов поручений из двадцати двух, остальным внятный отказ. Коммит 7e7007a2.
• Исполнитель плана для цели python лёг в дерево — flang/src/emit/python/flang_io.py. Саму программу С ПЛАНОМ цель python пока печатать отказывается (FLANG_PLAN_UNSUPPORTED): исполнитель ждёт печати. Коммит e84e290b.
• Три примера под настоящими фреймворками — examples/frameworks/: nestjs-orders, react-invoice, vue-roman. Доказанное ядро на flang печатается в JavaScript и работает под Nest, React и Vue; где проходит граница, сказано в README каждого примера: решение — на flang, сокет и отрисовка — у хозяина-фреймворка. Коммит 374e9aaa.
• ./ярлык доказуемость печатает одно слово — ДОКАЗУЕМ или НЕ ДОКАЗУЕМ — по трём числам, снятым прогоном, а не по суждению, вписанному в прозу. Коммит 7b03ee3a.
• ./ярлык версия X.Y.Z поднимает число версии в одном источнике и разносит его по производным местам — package.json, #define в C, страница man, формула Homebrew; сторож производных краснеет, если хоть одно отстало. Коммиты 3071b76c, d676ec12.

Что изменилось

• Переигрыватель гейтит равенства-постусловия по цепочке ходов. Раньше ложный ход под постусловием-равенством проходил кодом 3, неотличимым от честного, потому что переигрыватель звался нулём строк; теперь такой ход даёт код 1. Коммит 3931ae1a.
• Две придирки чекера закрыты: посылка под принцип … без явно написанной теорема до переигрывателя не доходила (ходы под ней были декорацией), а вставить_вместо безусловно оборачивал вставляемое тело лишней парой скобок, и на составном условии до цели не дотягивалось ни одно написание довода. Коммит 3cb04bcb.
• Семя пересевается быстро, без полной перепечатки, когда flang/self не тронут. Коммит d0060d56.
• Перечень команд flang сверяется сразу по пяти местам: страница man и оба README не знали команду new. Коммит fb29de4d.
• Девятая цель печати, elixir, взята под присмотр CI, и расхождение девяти целей на одной программе стережётся отдельным прибором. Коммиты 5a5e9a74, 532e6f2b.

Что сломалось

• Язык НЕ формально доказуемый, и это машинный вердикт, а не оценка: git grep -c перепиской flang/proof/checker/checker.c даёт 10, а не 0, и ./ярлык доказуемость отвечает НЕ ДОКАЗУЕМ. Взято 2 гейта критерия из 7.
• Узкий подкласс мест не мигрирован: маршрут «по объявлению» — 146 мест «доказано» из 159 — печатает только имя правила, без цепочки ходов, и переигрывателю нечего проигрывать.
• Оплата требует в новом приёме частичная: предусловие вызванной считается снятым, только если синтаксически совпало с одним из требует вызывающей. Погашение вычислением или охраной если эта волна не читает — такие места честно отвергаются кодом 1, а не принимаются по ошибке.

0.7.12 — 6 сентября 2026

Установка везёт рантаймы всех девяти целей печати, а не одной

Что появилось

• Обходчик примеров flang/self и работа CI при нём: 4350 примеров из 4445 под присмотром. До этого их не гонял пофайлово никто — ноль в CI. Полный прогон снят целиком: 55 минут 19 секунд, код 0, 12 530 примеров. Коммиты a35a4b42, ec039e7f, 3690acf4.
• Второй носитель приёма «разбором по случаям» — algebra, с пробами. Коммиты e11ed933, bb1e15a8.
• Два правила чекера: «начало по построению» значением, а не только тождеством, и «невыполнимая посылка» — из несовместимых допущений следует что угодно. По счёту записей корпуса это 28 записей из 86 против 30 из 86. Коммиты 2d58f99e, 3e2ac46c.
• Печать кеша приговоров называет попадания и промахи числом. Коммит c137e8d5.

Что изменилось

• Релизный архив кладёт каталог runtime/<цель>/ — 32 файла, 2 435 747 байт, — а формула Homebrew и плагин asdf переносят его корень целиком в share/flang. Раньше ставилась одна цель из девяти: остальные восемь обещаны в странице man, в обоих README и в справке двоичного, и у поставившего не работали. Коммит 11295873.
• Ключ кеша приговоров считается SHA-256 вместо многочлена: старый ключ при заявленных 59,79 бита подделывался за 3,6 секунды. Коммит deea0d61.
• Корпус перепечатан нынешним двоичным — 67 записей. Доля, проверенная чекером, 13,75 % → 17,77 % (обещали 17,92 %, разница от сдвинувшегося знаменателя): долю держали протухшие записи, а не чекер. Коммиты e1e362da, ed5de60a.
• Дыра «ходы без теоремы прячут долг» закрыта обеими половинами: «закрыта reduction» сверяется с исходником, а пустой «ход конец» больше не прячет долг. Коммит 817be78a.
• «Это число» дописано в список ввоза proofterm — 1289 примеров не шли никогда. Коммит a85c7bb4.
• Девятая цель печати дописана пяти сторожам, которые её не видели; там же нашлось, что цель cpp экранирует имена по списку цели c. Коммит 9fb0f293.

Что сломалось

• Язык по-прежнему НЕ формально доказуемый: чекер проиграл 30 записей корпуса из 86 при пороге гейта 95 %.
• В CI собираются и гоняются восемь целей печати из девяти; девятая на этот выпуск только названа числом, под присмотр она попала уже в 0.7.13. Коммит 6c0deb07.

0.7.11 — 5 сентября 2026

Надзор возвращён на dev, и сторожа доказывают прогоном, что умеют краснеть

Что появилось

• Хук .githooks/pre-push гоняет дешёвых сторожей перед пушем и вслух называет то, чего он НЕ проверил. Весь набор стоит около 134 минут раннера — такой хук обходили бы через --no-verify, и он был бы хуже никакого. Ставится одной командой: git config core.hooksPath .githooks. Коммит 1de3cf23.
• Прибор «у кого показано прогоном, что он краснеет»: сторож без пробы порчи — это сторож, которому верят зря. Коммиты ff354a73, 69550a3e, dc24ffa3, 83a838b2.
• Перепись «каких сторожей CI не зовёт»: число до этого считали рукой, и оно было неверным. Коммиты b29e8fa6, 3fa4c09f.
• Сторож производных версии: строка версии в семени систематически отставала от выпуска, теперь расхождение краснеет, а сама версия сверяется с АРТЕФАКТОМ выпуска, а не с файлом рядом. Коммиты 2532b671, cf337f76.
• Опись доказанного сверяет свою же таблицу с деревом и вписана в ярлык и в CI. Коммиты 1bfe1e7d, 5dba51a1, 2aa82f5c.

Что изменилось

• Чекер выучил три правила: отрицание замкнутого счёта, оговорка о конечности как посылка, «цель следует из объявленного о доводах». Доля корпуса, проверенная чекером, 7,50 % → 13,75 %. Коммиты 25181b19, ee23dd75, f5d378a1.
• Закрыта последняя названная дыра гейта Г2: довод индукции берётся ДО двоеточия. Отдельно закрыт ложный приём — объявление типа читалось сквозь примечание — и с ним пять ложных тревог. Расширенный замер даёт 62 ложные тревоги из 923 у старого чекера и 0 у нового. Коммиты 002b20f6, a54d4b55, 56a8441c.
• CI снова ходит по ветке dev: девятнадцать работ не проверяли ни один из 74 пушей. Сборка в CI стала вдвое быстрее, двоичный кешируется. Коммиты 8f90f49a, 15e89235.
• Синхронизация крана Homebrew записана в порядок выпуска: шесть выпусков подряд, с 0.7.4 по 0.7.10, ушли без неё, и brew install всё это время ставил 0.7.3. Коммит db23eb3b.
• Заметки о выпусках 0.7.x взяты с main целиком: они были написаны там и в dev не возвращались, потому что выпуск делается на main. Одиннадцать версий добавлены, ни одна не переписана. Коммит 532468f2.

Что сломалось

• Архив 0.7.11 так и не вышел, и релиза на GitHub у этого тега нет. Конвейер выпуска остановился на шаге «Сверить хеш архива с формулой Homebrew»: в формуле на теге стоял sha256 архива 0.7.10 (825a2b5b…, тот же, что и на v0.7.10) — ./ярлык версия sha256 намеренно не трогает, его вписывают отдельным коммитом после сухого прогона, и для 0.7.11 такого коммита не сделали. Следующий шаг, выкладку, конвейер пропустил; ничего битого не вышло, тег не удалялся.
• Язык по-прежнему НЕ формально доказуемый: доля корпуса, проверенная чекером, 13,75 % при пороге гейта 95 %. И держат её на этот момент не правила чекера, а протухшие записи корпуса — замер обещает от перепечатки 17,92 %. Коммит 7e369d98.
• Показано прогоном, что умеет краснеть, только у 8 сторожей из 58, и двадцати из непроверенных CI верил зря. Коммит ff354a73.
• Перепись сторожей на 5 сентября 2026: сторожей 56, CI зовёт 29, двадцать семь не зовёт никто. Коммит 3fa4c09f.

0.7.10 — 4 сентября 2026

Хотфикс: живая оболочка падала на каждой строке ввода

Что изменилось

• REPL (flang без доводов) отвечал FLANG_UNKNOWN_NAME: запись не содержит поле «планировщик заголовок» на ЛЮБОЙ ввод, включая 1 плюс 1 — не только сложные примеры. Причина: ручной список полей записи «Настройки» в flang_repl.c (используется печатью цели «c» для каждой строки живой сессии) отстал от общей таблицы полей на два имени, когда цель «c» выучилась печатать процессы. Починка landed на dev 3 сентября, но приземлилась ПОСЛЕ тега v0.7.3 — в нём баг был живой.
• Строка версии в семени (FLANG_VERSION) отстала на три релиза (0.7.0 вместо 0.7.3) — тот же класс беды, что уже чинил хотфикс 0.7.1, снова закрался и снова починен; заведена задача, чтобы это не повторялось в четвёртый раз.

Что сломалось

• Язык по-прежнему НЕ формально-доказуемый: взято 2 из 7 гейтов критерия. За это время найдена и починена настоящая дыра в независимом чекере (сокрытие текста за примечанием проходило непроверенным ещё в одном месте), доля корпуса, проверенная чекером, поднята с 5,00 % до 7,50 %, и впервые сошлась побайтово пара из двух независимых печатей одного коммита — но ни один гейт целиком этим не взят.

0.7.9 — 4 сентября 2026

Метка есть, публикация остановлена конвейером

Что изменилось

• Тот же материал, что вышел как 0.7.10 — шестая подряд непубликация в этой цепочке (после v0.7.4-v0.7.8), пока не нашёлся настоящий путь: у release.yml workflow_dispatch не снят (снят он был только у старого publish-npm.yml), и сухой прогон на ветке даёт настоящий хеш без сожжения тега. Конвейер каждый раз останавливался ДО публикации, ничего битого не вышло; тег не удалялся, просто пропущен.

0.7.8 — 4 сентября 2026

Метка есть, публикация остановлена конвейером — намеренно

Что изменилось

• Метка поставлена сознательно с заведомо чужим хешем (архива 0.7.7), чтобы получить настоящий хеш архива 0.7.8 из текста ошибки конвейера. Заодно найдено: конвейер требует точного совпадения версии тега и package.json ДО сборки архива — версию нельзя было оставить прежней, чтобы сохранить силу хеша. Тот же материал реально вышел как 0.7.9.

0.7.7 — 4 сентября 2026

Метка есть, публикация остановлена конвейером — намеренно

Что изменилось

• Метка поставлена сознательно с заведомо чужим хешем (архива 0.7.6), чтобы получить настоящий хеш архива 0.7.7 из текста ошибки конвейера — тем же приёмом, каким и так уже дважды снимался хеш этой ночью. Тот же материал реально вышел как 0.7.8.

0.7.6 — 4 сентября 2026

Метка есть, публикация остановлена конвейером

Что изменилось

• Число в Homebrew-формуле было хешем архива 0.7.5 (координатор перепутал версию содержимого при копировании числа из ошибки конвейера) — при своей же сборке на теге содержимое, разумеется, разошлось. Конвейер остановился ДО публикации, ничего битого не вышло. Тег не удалялся, просто пропущен.

0.7.5 — 4 сентября 2026

Метка есть, публикация остановлена конвейером

Что изменилось

• Тот же материал, что вышел как 0.7.6: sha256 в Homebrew-формуле снят локально документированной командой, но местная сборка архива не совпала побайтово с тем, что даёт конвейер (причина не разобрана) — конвейер остановился ДО публикации, ничего битого не вышло. Тег не удалялся, просто пропущен.

0.7.4 — 4 сентября 2026

Метка есть, публикация остановлена конвейером

Что изменилось

• Тот же материал, что вышел как 0.7.5: sha256 в Homebrew-формуле стоял от 0.7.3, конвейер выпуска сверил его с архивом, который сам собрал на теге, и остановился ДО публикации — прибор сработал как задуман, ничего битого не вышло. Тег не удалялся (запись запрещена), просто пропущен.

0.7.3 — 3 сентября 2026

Хотфикс версии дошёл до публикации

Что изменилось

• Тот же хотфикс версии, что метился как 0.7.1 и 0.7.2, наконец опубликован: у обеих меток ручная сборка архива не совпала с тем, что собрал сам конвейер выпуска (0.7.1 — расхождение полное, 0.7.2 — 4 байта из 4 447 763, причина не разобрана), и Homebrew-формула не проходила проверку. Для 0.7.3 sha256 взят напрямую из sha256sum самого конвейера, а не пересчитан вручную — установка проверена целиком: скачивание, сверка хеша, сборка, flang --version.

0.7.2 — 3 сентября 2026

Метка есть, публикация снова не дошла

Что изменилось

• Вторая попытка опубликовать хотфикс версии 0.7.1: реальный sha256 архива взят с конвейера, а не пересчитан руками. Сборка разошлась с конвейером на 4 байта из 4 447 763 (причина не разобрана) — Homebrew-формула не проходила проверку. Тег не удалялся (запись запрещена), просто пропущен: пользователям, ставившим через Homebrew, эта метка ничего не дала.

0.7.1 — 3 сентября 2026

Хотфикс версии — тег вышел, публикация не дошла

Что изменилось

• flang --version отвечал «0.6.2» под выпуском 0.7.0 — на два релиза позади: строку версии в семени забыли бампнуть вместе с package.json. Задача 9959 чинит её. Заодно исправлена версия Homebrew-формулы (0.6.2 -> 0.7.0, пропущенная при первой правке), версия на сайте и часть работ CI, жёгших часы на пуш без имени.

Что сломалось

• Публикация этой меткой НЕ дошла: ручная сборка релизного архива не совпала с тем, что собрал сам конвейер выпуска, и Homebrew-формула не проходила проверку хеша. Тег не удалялся, просто пропущен — успешно эта же починка опубликована только в 0.7.3.

0.7.0 — 3 сентября 2026

Компилятор перепечатан начисто, а главная работа выпуска — поиск собственных обманов

Что появилось

• Девятой целью печати стал C++; появились регулярные выражения, драйверы sqlite и Redis, TLS 1.3 и реестр пакетов.
• У файлов три равноправных расширения; у пределов шагов и глубины — свои ключи; --no-check печатает без проверки, а check --быстро честно говорит, чего он не смотрел.

Что изменилось

• Компилятор перепечатан начисто с замороженного ствола: печать шла 12 часов 4 минуты, из них 10 часов 25 минут (86 %) заняла стадия «Суд ядра о программе».
• Выпускной путь впервые прошёл целиком. Прежде он не проходил ни разу: шаг сборки архива звал двоичный, которого никто не собирал, и релиз 0.6.2 собирали руками.

Что сломалось

• Язык НЕ формально-доказуемый: из семи гейтов критерия взято два — ядро выдаёт объект доказательства и размер доверия назван числом.
• Ядро способно доказать ЛОЖЬ: при развёртке вызова оно подставляет довод под связыватель того же имени и печатает «доказано обо ВСЕХ входах» про утверждение, ложное на каждом входе. В сегодняшнем корпусе таких доказательств нет — померено, 0 из 240.
• Доля корпуса, проверенная независимым чекером, — 0,00 % на момент заморозки. Прежде называвшиеся 0,83 % завышены и сняты.
• Чтобы перепечатать компилятор семенем 0.7.0, нужен ключ --предел-глубины 200000: вшитый предел 20 000 упирается в одну машинную строку постусловия в 90 286 знаков.

0.6.2 — 22 августа 2026

Установка через Homebrew починена: архив приезжал с каталогом, в который нельзя войти

Что появилось

• Защищённое соединение работает живьём: двенадцать прогонов с настоящими кодами ответа.
• Принцип свёртки усилен пройденным куском списка: +2 доказанных обещания, при правиле заведены подделка и честная половина.

Что изменилось

• Две меры длины строки сведены к одной. Попутно найдена и закрыта порча памяти.
• Разведка ввозов разбирает шапку файла, а не файл целиком: память проверки −24 %, время −5 %.
• Сняты две рукописные копии сличения списков и исправлены три устаревшие ссылки на давно снятый запрет.

Что сломалось

• Ничего. Этот выпуск чинит установку, сломанную в 0.6.0 и 0.6.1: архив собирался режимом --mode=u=rw,go=r, который снимает право входа и с КАТАЛОГОВ, поэтому runtime-c приезжал как drw-r--r-- и brew install падал с Errno::ENOENT: runtime-c/flang_cli.c. Лечится буквой X — --mode=u=rw,go=r,a+X. Команда исправлена и в формуле, и в конвейере публикации; довод записан рядом с ней.

0.6.1 — 22 августа 2026

Правка компилятора, не доехавшая до собранного, теперь краснеет за полсекунды

Что появилось

• Дешёвая сверка исходников компилятора с его переводом на C: sh scripts/bootstrap-reprint.sh --bystro. Прежде расхождение ловилось только часовой перепечаткой, и за двое суток работа четырежды уезжала в ствол правилом, которого в собранном компиляторе не было. Теперь это видно сразу и на каждом пуше.
• Два новых правила у проверяльщика доказательств: разбор случаев по внутреннему условию цели и правило несовместимых условий. Прибавка измерена и записана числом в самом ядре: +2 и +2 доказанных обещания на шести файлах библиотеки.
• Октетная пара поручений у файлов: читать и писать файл байтами, а не текстом. Текстовая пара на нетексте теперь честно отказывает вместо тихой порчи, а нулевой октет вернулся в законный текст — отказ только на неправильном UTF-8.

Что изменилось

• Проверка столкновений имён видит всё замыкание: ввоз по имени без пути разрешается реестром, и вместо одного файла из тридцати шести она смотрит все. На этом дереве — 736 файлов и 56 345 объявлений.
• Проверка подделок смотрит весь каталог, а не список: названных подделок было 15, стало 24, и обрыв на первой несложившейся больше не прячет остальные.
• «Ответить в соединение» перестало рвать содержимое по первому нулевому байту: длина берётся у самого значения. Замерено на собственном исходнике компилятора — ствол терял 47 184 байта на flang/self/link.flang.

Что сломалось

• Текстовые поручения чтения и записи файла на двоичном содержимом теперь отказывают, а не возвращают обрезанное. Для двоичного есть октетная пара.

0.6.0 — 22 августа 2026

Долгие вычисления перестали упираться в память: 15,98 ГиБ ушли в 0,0135

Что появилось

• Вход в PostgreSQL по scram-sha-256: SHA-1, HMAC, PBKDF2 и клиент SCRAM написаны на самом языке, а вход проверен прогоном против настоящей PostgreSQL 17.10, а не заглушки.
• Три новых правила вывода у проверяльщика доказательств. Оговорка о конечности: «не число» стоит вне порядка, всякая граница на нём ложна, и оговорка «пока это число» теперь читается фактом. Разбор случаев по дизъюнкции в допущении: «А или Б» не расщепляется, а разбирается надвое, и цель принимается только когда сошлись оба случая. Цель «А и притом Б».
• Надзор за упавшими процессами поверх сети: узел переживает смерть соседа, а работу пропавшего забирает выживший. Пропажу надзору отдаёт доклад слоя связи, а не уборка сокета.
• Модуль «Провод» — общая половина двоичных протоколов поверх TCP, вынутая из драйвера PostgreSQL. Из 83 функций драйвера про сам PostgreSQL оказались 39; остальное годится любому двоичному протоколу.
• Браузерные страницы написаны на самом языке: восемь целей печати из восьми, ни одной строки JavaScript в самих страницах.
• Проверка пустых доказательств. 93 доказанных утверждения библиотеки разложены на четыре кучи, и «доказано» о том, что верно про любую функцию с такой же подписью, названо своим именем, а не сосчитано наравне с содержательным.

Что изменилось

• Память при долгом вычислении перестала расти. Интерпретатор — это цикл, и область памяти освобождалась только в самом конце: хвостовая рекурсия стоила 84 килобайта на виток. Теперь она освобождается на каждом витке. На 200 000 витков пик был 15,98 ГиБ, стал 0,0135 ГиБ, время упало с 25,3 до 13,5 секунды, а от числа витков пик не зависит вовсе.
• Равенство в теле функции разрешено: прежний запрет оказался устаревшим ограничением, а не границей языка. Разрешение считать по-прежнему не означает разрешения выводить — подделка на это заведена.
• Потолок шагов при печати компилятора поднят с 40 миллионов до миллиарда. После новых правил вывода проверка компилятора самим собой перестала помещаться в прежний, и печать отменялась целиком.
• Реализация проверок на JavaScript снята: слой доказательств (4958 строк), проверки печати и занятых целью имён (682 строки) и четыре файла, которых не звал никто (836 строк). Печать компилятора в C не требует Node ни на одном шаге.
• Поиск по кодам отказа в документации находит 13 кодов из 13 — было 0 из 13.

Что сломалось

• Ярлык emit:check убран: проверку печати делает pechat:check на самом языке, а occupied:check зовёт scripts/guards/occupied-names-guard.flang вместо снятого скрипта на JavaScript.
• Общая половина драйвера PostgreSQL уехала в модуль «Провод». Программы, звавшие «Знак байта», «Четыре октета», «Два октета» и соседей прямо у «Разговора с базой», должны ввозить «Провод».

0.5.1 — 19 августа 2026

Установка на macOS починена: 0.5.0 не собирался там ни у кого

Что появилось

• «Открыть соединение» — поручение, которым программа сама идёт к чужой службе по сокету. До него на flang нельзя было написать клиент к базе данных или к любой службе с двоичным протоколом: служба умела отвечать, но не спрашивать.
• Вся четвёрка сетевых поручений переименована на одно слово: «Открыть соединение», «Принять соединение», «Прочитать из соединения», «Ответить в соединение».
• Вторая дверь у напечатанной программы на C — МОДУЛЬ_enter: она сверяет аргументы с объявленными типами. Прежде чужой код, слинкованный с библиотекой, получал на −3 для нат ответ 1 и не узнавал об этом.

Что изменилось

• Пакет в npm называется @digitable-lol/flang, а не @digitable-lol/fts: язык называется flang.
• Файлы C зовутся compiler_flang.[ch] вместо kompilyator_flang.[ch] — транслит ушёл из имён, и печать стала меньше на 124 431 байт.
• Сборка выхода зовётся flang, а не flang_cli; формула Homebrew и плагин asdf принимают оба имени.

Что сломалось

• Ничего из объявленного прежде. Двоичный по-прежнему печатает только в C и не берёт составные значения в --args — обе границы названы на страницах установки и в man.

0.5.0 — 18 августа 2026

Компилятор считает себя сам, а напечатанный код стал быстрее и экономнее

Что появилось

• Каждая из восьми целей печати теперь написана и на самом flang: последним закрыт js. Целей, у которых своей версии на flang нет, не осталось.
• Отчёт о доказательствах считается кодом на самом flang: flang check --proof больше не зовёт реализацию на JavaScript.
• Тип вес — отрезок от нуля до бесконечности. Три действия над ним разрешены, четыре отказывают и показывают пару, на которой отказали.
• Точные десятичные: деньги считаются без двоичной дроби, и двоичный берёт их сам.
• Разрешение «повторить безопасно» выдаётся явно, а не подразумевается.
• Замок зависимостей: программа собирается из него без исходников.
• Ввод-вывод дорос до перечисления каталога и запуска процесса, а flang io разными кодами выхода отличает «нашёл беду» от «сам сломался».
• Сайт документации собирается из docs/ одной командой, без единой зависимости.

Что изменилось

• Напечатанный C стал быстрее: межмодульная оптимизация включена умолчанием — это 1,14 раза, — а проверка типа не печатается там, где тип уже доказан: на арифметике это 4,9 раза, вместе 1,6.
• Область памяти в цели C научилась откатываться: сортировка слиянием четырёх тысяч чисел берёт 3,5 МиБ вместо 1655.
• Объявленный предел глубины в WebAssembly стал пределом: 7474 вложенных вызова и тот же текст отказа, что при обычном запуске, вместо смерти вкладки на глубине 60.
• Диагностика цитирует слово той поверхности, на которой написан файл: расхождений 0 из 186.
• Языковой сервер перестал отвечать нулём байт и кодом 0 на непонятый довод.

Что сломалось

• Слово требует стало ключевым. Программа, в которой это было своё имя, больше не разбирается.

0.4.8 — 9 августа 2026

Вложение и пересечение: у множеств появились слова

Что появилось

• У множеств появились слова: вложение и общая часть — и работают они по причине, а не по списку.
• Объявленная мера: убывает <выражение>. Цикл доказывается ей там, где двух даровых порядков не хватило.
• Логика пишется инфиксом: не, и притом, или.
• Кодовая точка символа стала числом — строкам не хватало именно этого.
• У процесса своя куча: сообщение уезжает в неё копией, а исчерпание кучи стало отказом процесса, а не смертью программы.
• Ящик ограничен объявляемым размером, и переполнение стало отказом отправителя.
• Словарь стал логарифмическим: дерево поиска с приоритетом по хешу ключа.

Что изменилось

• Горячая замена работает под живым планировщиком, а состояние переезжает проверенной функцией.
• Компилятор, напечатанный в C, ставит проверку убывающей меры и больше не зацикливается там, где реализация на JavaScript отказывала.

Что сломалось

• Слово убывает стало ключевым.

0.4.7 — 7 августа 2026

Монада, отказ значением, полиморфизм

Что появилось

• Монада получила форму: в монаде разворачивается в разбор до конца разбора.
• Отказ «к числу» стал значением: столбец из строк складывается, не падая.
• Число убывает на постоянный шаг — до проверенного дна.

Что изменилось

• тотальная перестала обещать больше, чем доказано: где завершение держится числом, в код печатается проверка убывающей меры.
• Библиотека схлопнулась по типам после закрытого полиморфизма; второй параметр нашёл дефект в самоприменении.

0.4.6 — 7 августа 2026

Бинарник разговаривает с человеком: check, оболочка, справка, man

Что появилось

• Установленный бинарник стал инструментом для человека: flang check, справка, версия, страница man.
• Функция стала значением: компилятор заменяет её меткой и разбирает по меткам, поэтому граф вызовов остаётся конечным, а функция-значение доехала до всех целей печати.
• В языке появился словарь.
• Логические операции появились функциями — слово «и» в языке уже занято.

Что изменилось

• Самоприменение понимает полиморфизм и высший порядок.
• Связывание перестало терять теоркат на границе файла: доказательство переживало её и не должно было.

0.4.5 — 7 августа 2026

Оболочка в установленном бинарнике, ввод-вывод и процессы на BEAM

Что появилось

• Оболочка есть в бинарнике, который ставится готовым: язык можно потрогать сразу после установки.
• Язык научился читать файл и ходить в сеть, не перестав быть чистым.
• Надзор перестал быть объявлением: упавший процесс поднимается к тому же началу.
• Процессы поехали на настоящей BEAM через печать в Elixir, и сверка идёт по набору исходов.
• Типы стали параметрическими — без этого монада была невыразима.

Что изменилось

• Лексер стал тотальным целиком: слои самоприменения перестали ходить по строке позицией.
• Четыре задачи и стандартная библиотека стали тотальными.

0.4.4 — 6 августа 2026

Языковой сервер, функтор с законами, конкурентность

Что появилось

• Языковой сервер для .flang: та же проверка, что у flang check, прямо в буфере.
• Конкурентность: атомарность по процессу, а не глобальная, и печать в BEAM.
• Функтор перестал быть словом без гарантии: у него появились законы, и они проверяются.

Что изменилось

• Двунаправленные управляющие символы больше не печатаются сырыми в java, csharp и elixir: подмена исходника невидимым знаком закрыта во всех целях.

0.4.3 — 6 августа 2026

Подсветка для Vim едет в пакете

Что появилось

• Подсветка едет в пакете: 154 слова языка, и различимость ролей проверяется.
• Оболочка flang repl: язык можно потрогать, а не только запустить файл.
• Встроенная форма «разложить … на символы» — посимвольный проход стал доказуемым.

0.4.2 — 6 августа 2026

Целей печати стало восемь, а компилятор ставится без Node

Что появилось

• Печать в Java, C# и Elixir — целей стало восемь.
• Компилятор ставится без Node: релизный C и формула для установщика.

Что изменилось

• Компилятор, написанный на самом flang, напечатал сам себя без единого расхождения.
• Описание пакета отставало на пять целей печати — исправлено.

0.4.1 — 5 августа 2026

Команды пакета отвечают после установки

Что изменилось

• После установки команды печатали ноль байт и выходили с кодом 0: страж точки входа сравнивал пути как строки, а установщик кладёт команды символьными ссылками. Закреплено проверкой, которая ставит ссылку так же.

0.4.0 — 5 августа 2026

Первая публикация

Что появилось

• Пакет несёт язык вместе с инструментами FTS: 327 файлов, 1,1 МБ в архиве и 8,3 МБ распакованным.
• Печать в C, Go, Rust и Python.
• Связывание модулей: использует, и выборочный ввоз только.
• Самоприменение: лексер, разборщик, проверка типов, анализ тотальности и печать в C — написаны на самом flang.
• Команда emit: печать в целевой язык из командной строки.