flang язык, в котором спецификация исполняется

flang

flang — язык программирования с исполняемой спецификацией. Его отличительная черта — разделение программ на два класса, которые различает компилятор: программы, завершение которых доказано, и все остальные. Поверхность языка словесная: в синтаксисе нет символов, которые нельзя набрать на обычной клавиатуре.

Язык вырос из FTS (Formal Type Surface) — языка исполняемых спецификаций для описания предметных областей. FTS остаётся тотальным подмножеством flang: любая модель .fts является валидной программой языка и вычисляется одинаково обеими реализациями.

Парадигмафункциональная, декларативная
Появилсяавгуст 2026
Типизациястатическая, сильная, суммы и произведения типов
ЛицензияBSD 2-Clause
Расширения файлов.flang, .fts
Репозиторийgithub.com/digitable-lol/flang

Особенности

Два класса программ

Компилятор различает функции с признаком тотальная, для которых доказано завершение на любом входе, и обычные функции с произвольной рекурсией.

Доказательство ведётся двумя способами. Структурное убывание: каждый рекурсивный вызов получает структурно меньший аргумент — хвост списка, поле записи, поле варианта. Числовая мера: аргумент уменьшается на постоянный шаг (н минус 1 — или н минус ш, если ш приходит в вызов неизменным и строго больше нуля) и снизу ограничен проверкой-неравенством. Что не берут оба, то отвергается: размер минус позиция уменьшается, но постоянного шага у него нет — позиция растёт от витка к витку, и обосновать этим завершение нельзя без рассуждений, которых компилятор не ведёт.

Разделение имеет прямое следствие: во встраиваемом режиме проверки фактов допускаются только тотальные функции. Система, отвечающая на вопрос «подтверждено или нет», не имеет права зависнуть.

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

Печать в целевые языки

Программа печатается в исходный код на восьми языках: C, Go, Rust, Python, Java, C#, Elixir и JavaScript.

Печать сопровождается дифференциальной сверкой: напечатанный код обязан давать те же значения, те же коды и те же тексты ошибок, что интерпретатор. Для каждой цели это проверяется на 35 программах, 214 функциях и 3071 точке сетки входов, а сетка строится не только из примеров, но и из порчи каждого аргумента заведомо чужими значениями — иначе диагностики остались бы непроверенными.

Такая сверка находит дефекты, невидимые для тестов отдельно взятого бэкенда. За время разработки так были найдены: печать некомпилируемого C при совпадении имени варианта и функции; литерал варианта, превращавшийся в запись в бэкенде Go; знаковый ноль при делении на бесконечность в Elixir.

Словесный синтаксис

В синтаксисе используются только слова: из … в …, после, цепочка … сначала … затем …, сохраняет композицию. Русская и английская поверхности равноправны и компилируются в одно синтаксическое дерево.

Категорная поверхность

Морфизм объявляет стрелку между объектами категории; композиция записывается словом после, а длинная цепочка — в порядке чтения:

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

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

Стыковка композиции проверяется компилятором и относится к доказанному: «б» после «а» собирается тогда и только тогда, когда кодомен «а» равен домену «б». Несостыковка называет, что с чем не сошлось:

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

Функтор отображает объекты и стрелки, и три его закона относятся к доказанному, а не к проверенному на примерах: образ стрелки обязан вести из образа домена в образ кодомена, образ композиции обязан быть композицией образов в том же порядке, образ единицы — единицей образа. Доказательство здесь возможно потому, что морфизм — объявление, а не значение: домен и кодомен известны до запуска, и законы проверяются сравнением объявлений, без сетки и без решателя. Имена категорий при этом остаются пометкой для читателя: категория отдельной сущностью не объявляется, и утверждать принадлежность объекта именно ей не на чем.

Моноид объявляется носителем, операцией и единицей; с обращением он становится группой — отдельного слова нет, потому что группа и есть моноид с обращением. Здесь граница «доказано / проверено» проходит внутри одной конструкции: доказывается устройство (операция — функция двух аргументов носителя, единица — значение носителя), а сами законы — ассоциативность, нейтральность, обратимость — проверяются на конечной сетке из примеров операции. Доказать их нельзя: это равенства вычислений на всех значениях носителя.

Изоморфизм и бифунктор объявляются и проверяются тем же сличением объявлений. У изоморфизма при этом само равенство «обратный после прямого = единица» не проверяется вовсе — ни доказательством, ни на сетке: у стрелки категории нет тела, вычислять нечего. Это допущение автора, и компилятор отвечает лишь на то, осмысленно ли оно сформулировано.

Отношения множеств сказаны двумя словами. вложение «В» из «А» в «Б» — это подобъект: стрелка, которая ничего не склеивает, то есть «А» и правда ЧАСТЬ «Б», а не его фактор. пересечение «П» из «А» и «Б» в «У» — расслоенное произведение: общая часть двух множеств ВНУТРИ объемлющего, и объемлющее здесь обязательно, потому что значения разных типов несравнимы и общий элемент иначе не с чем сличать. Граница проходит внутри обоих слов: устройство доказывается сличением объявлений, инъективность вложения и непустота общей части проверяются на значениях автора (склейка — предъявленный контрпример и потому ошибка; ненайденный свидетель — не ошибка, потому что «не нашли» это не «нет»), а универсальность общей части остаётся допущением автора. Объединения среди слов нет: ко-произведение в языке уже есть — это тип … вариант … вместе с исчерпывающим разбором.

Монада объявляется на параметрическом типе и называет две функции — возврат (η) и соединение (μ). Граница «доказано / проверено» проходит здесь так же, как у моноида: доказывается устройство — тип параметричен, возврат ведёт из «А» в M«А», соединение из M(M«А») в M«А», — а левая единица, правая единица и ассоциативность связывания проверяются на конечной сетке из примеров автора, с контрпримером в сообщении.

Отображение эндофунктора при этом не объявляется вовсе: у полиномиального функтора оно ровно одно, и компилятор выводит его из устройства типа. На том же стоит форма в монаде — do-нотация словами, где каждое пусть есть связывание, а последняя строка возврат есть η. Форма разворачивается компилятором ВНУТРИ разбора, в обычные вызовы поверх обычного разбор, поэтому печать во все восемь целей и оба слоя самоприменения получают её даром, а функций первого класса ей не требуется: тело продолжения известно синтаксически. Подробности и границы — flang/cat/MONAD.md.

Естественные преобразования описаны в контракте flang/cat/SPEC.md и не реализованы. Причина сместилась: раньше мешал сам параметрический полиморфизм, теперь он есть — и в языке, и в самоприменении, и в стандартной библиотеке. Мешает то, что checkMorphisms и checkFunctors знают имя типа, а не применение: домен морфизма ищется как ctx.records.has(имя), а «из функтора «Список» в функтор «Возможно»» — утверждение про применения. Это фаза 3 в flang/cat/POLY.md.

Разбор суждений

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

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

Диагностика выдаётся в JSON с кодом, уровнем и местом, поэтому пригодна для машинного разбора — это существенно для сценария, где код пишет не человек.

Реализации

Существуют две реализации, и обе поддерживаются намеренно.

Эталонная написана на TypeScript и JavaScript. Служит определением поведения языка.

Самоприменяющаяся написана на самом flang: лексер (84 функции), парсер (374), проверка типов (277), анализ завершаемости (124), печать в C (326), печать в Go (182) и связывание модулей. Ядро FTS переписано отдельно — 300 функций, все тотальные, с побайтовым совпадением вывода с эталоном на каждой модели репозитория.

Печать в Go — второй печатник, и функций у него 182 против 326 у первого не потому, что Go проще, а потому, что он импортирует печать в C: разбор AST, транслитерация имён, компоненты сильной связности графа вызовов и сбор объявлений у восьми целей устроены одинаково и уже сверены побайтово. Своим осталось то, чем Go отличается от C, — идентификаторы с ролью в имени, ошибка как значение, math.Copysign(0, -1) вместо минус нуля константой.

Лексер самоприменения тотален целиком — 84 функции из 84, — и это стоит отметить, потому что раньше их было 54 из 88. Разница ровно в одном: посимвольный проход перестал ходить по позиции. Убывала разность «размер минус позиция», то есть число; теперь строка раскладывается в список, и рекурсия по хвосту доказывается.

В августе 2026 года для самоприменяющейся реализации сошлась неподвижная точка: компилятор, напечатанный эталоном, печатает собственные исходники, и результат совпадает побайтово с третьим проходом — все семь файлов. Это означает, что компилятор понимает язык так же, как эталон.

Эталонная реализация не удаляется: относительно неё и проверяется схождение.

Установка и переносимость

Релиз содержит компилятор, уже напечатанный в C99, поэтому установка требует только компилятора C:

brew install digitable-lol/tap/flang

Node.js для установки не нужен. Такой способ распространения применяли и другие самоприменяющиеся языки: Go долго возил сгенерированный C, Nim возит до сих пор. Проблема начальной загрузки остаётся у тех, кто развивает сам язык.

Проверка живёт прямо в этом бинарнике: flang check файл.flang проходит разбор, связывание, типы и завершаемость и печатает замечания словами — с кодом и местом. Команды перечисляет flang --help, подробно описывает man flang.

Оболочка flang repl есть и здесь: вычислителя в бинарнике нет, поэтому она печатает сессию в C, собирает её системным cc против поставленного рядом рантайма и запускает; без cc она продолжает проверять разбор, типы и завершаемость.

Полный инструментарий — восемь бэкендов, интерпретатор и сервер MCP — распространяется через npm и требует Node:

npm install -g @digitable-lol/fts

Рантайм не содержит архитектурно-зависимых конструкций; выравнивание вычисляется объединением базовых типов, то есть берётся максимальное для платформы. Компилятор собран кросс-компилятором под RISC-V и запущен под эмуляцией без единой правки исходного кода: значения совпали с x86-64 до последнего знака, включая 0.1 плюс 0.2 = 0.30000000000000004, NaN и Infinity.

Ограничения

Функции первого класса есть и печатаются во все восемь целей. Ограничение снято дефункционализацией: значение-функция — это тег, применение — диспетчер по конечному списку тегов. Поэтому цели без замыканий не страдают, и доказуемость завершения тоже: список тегов конечен, программа видна целиком, и анализ завершаемости не изменился ни на строку — изменилось, чем он питается.

Печать понижает программу ОДНИМ проходом перед бэкендами: тег становится вариантом, применение — вызовом диспетчера, и ни один из восьми бэкендов высшего порядка не видит вовсе. На программе без функций-значений проход возвращает тот же объект, поэтому печать остального не может измениться по построению — это проверено побайтово на всех программах репозитория.

Одно расхождение названо и оставлено: тег, которого программа не строит, можно подать снаружи, и отвергают его обе стороны, но разными кодами — вычислитель своим, напечатанный разбор своим. Свести их значило бы завести встроенную форму «возбудить ошибку с этим текстом» и править восемь рантаймов, то есть ровно то, ради отсутствия чего проход и написан. На значении, которое программа способна построить сама, расхождения нет.

Параметрический полиморфизм работает и в репозитории. Параметры типа объявляются у типов и у функций, применяются, выводятся при вызове, и печать их не стоит ничего — все восемь целей типы и так стирают. Долгое время пользоваться этим было нельзя: парсер самоприменения полиморфизма не понимал, а корпус сверки собирается по маске каталога, поэтому первый же такой файл в библиотеке ронял неподвижную точку. Теперь понимает — и монада выразима: тип «Возможно» от «А», функция «Обернуть» от «А», связывание с параметром типа функция из «А» в («Возможно» от «Б») проходят разбор, типы и завершаемость. Библиотека на это переведена: flang/stdlib/optional.flang — это «Возможно» от «А», flang/stdlib/result.flang — «Результат» от «Значение» и «Беда», функций столько же, а примеры у семи из них записаны сразу на двух типах и считаются одним телом. С 8 августа 2026 то же сделал и flang/stdlib/higher-order.flang: подстановка выводится из самих значений примера, и «Отобразить» с «Отобразить строки», «Отфильтровать» с «Отфильтровать строки» — четыре функции с попарно одинаковыми телами — стали двумя, не потеряв ни одного примера. Что схлопнуть НЕ вышло, названо там же в шапках и подтверждено программами в flang/test/claims.test.mjs: равен над параметром типа отвергается (отсюда sets.flang и dictionary.flang остались про строки), а начальное значение свёртки типизируется без ожидаемого типа.

Пользовательские свойства проверяются, а не доказываются. Доказываются завершение, типы, стыковка композиции и три закона функтора — это утверждения обо всех входах, и берутся они из объявлений. Пользовательские свойства и примеры проверяются на конечной сетке входов; на ней же сверяется согласие интерпретатора с бэкендами. Законы моноида, монады, изоморфизма и отношений множеств тоже идут сеткой — из значений, написанных автором, с названным пределом. Законов естественного преобразования нет вовсе: самого слова в языке пока нет. Документация обязана различать эти случаи: «проверено на N входах» — не то же самое, что «доказано».

И различать это обязана не только документация. flang check --proof печатает ведомость доказательства: по каждой функции — чем именно несётся её обещание тотальная (композицией, если рекурсии нет; структурой; постоянным шагом со сторожем; объявленной мерой со сторожем), по каждому закону — размер сетки, на которой смотрели, вместе с её пределом, а отдельным списком — то, что принято на веру и не посчитано ничем. Слова в ведомости не взаимозаменяемы: «доказано» стоит только у утверждений про все входы, у сетки не стоит ни «доказано», ни «проверено» — там сказано «сетка N значений: нарушений не найдено», потому что «не нашли» и «нет» — разные утверждения. И «не найдено» означает «ИСКАЛИ и не нашли»: примеры при утверждении прогоняются тем же вычислителем, каким работает flang test, а найденный контрпример печатается словом «НАРУШЕНО» и бьёт любой вердикт, включая «доказано». Где прогона не было, так и написано — «нарушений не искали». --json отдаёт ту же ведомость машине: этапы работы над доказуемостью меряются её числами, а свод по всему корпусу печатает flang/scripts/proof-ledger.mjs.

Цепочку шагов можно не писать руками, а ПОИСКАТЬ: flang/scripts/proof-search.mjs перебирает обоснования и печатает найденное доказательство теми же словами языка, которыми его пишет человек, — хоть впиши в файл, хоть прочитай глазами. Поиск при этом стоит СНАРУЖИ языка и в контур доверия не входит: ведомость от него не меняется ни на строку, а найденное принимает не он, а то же самое ядро, которым проверяется написанное рукой. Соврёт — отвергнет ядро, и слово «доказано» не появится; поэтому корректность поиска доказывать не надо, и написан он может быть как угодно.

Ведомость есть и на самом flang — flang/self/proof.flang. Она печатает то же и теми же словами: на одной программе с одними итогами анализа её текст совпадает с текстом ведомости на JavaScript знак в знак, а машинный вид — байт в байт, вместе с порядком ключей (flang/test/self-proof.test.mjs). Носители обещания при этом называет цепочка, в которой JavaScript ничего не считает: self/totality.flang выносит вердикт, self/carriers.flang записывает, чем он вынесен, а ведомость по нему отчитывается. Сама она тотальна целиком, обычной функции нет ни одной — программа, печатающая доказательства, обязана проходить тот самый анализ, чьими выводами она отчитывается. Объявленную меру самоприменённый анализ теперь и разбирает, и ПРОВЕРЯЕТ: компоненту он принимает по мере автора, а печать ставит на такой вызов полиморфного сторожа с тремя постусловиями — «не убыла», «ушла ниже нуля», «перестала быть целой».

Что свод говорит про дерево сегодня: тотальных функций 5034 из 6585, и обещание 4619 из них несёт композиция — рекурсии в них нет, доказывать нечего. Рекурсивных 415, и здесь начинается разница: у 326 убывание несёт структура значения — статически, без сторожа; у 22 его несёт точный шаг на объявленном нат — тоже статически и тоже без сторожа, потому что дно и потолок даёт сам тип; а у 67 остаётся сторож в 101 местах, из них 3 на постоянном шаге и 64 на объявленной мере. Пятый носитель появился вместе с точным натуральным типом и снял пятнадцать мест сторожа, не добавив ни одного: переполнение там, где натуральное производится, ловится расширением типа, а не проверкой в напечатанном коде. Доля объявленной меры выросла с трёх функций до шестидесяти четырёх за один день: партия решений LeetCode 2026-08-12 добавила 56 задач, а скользящее окно, таблица динамики, двоичный поиск по разделяющей позиции и заливка сетки доказываются именно мерой — структуры значения им не хватает. Законов, посчитанных на сетке, восемь; принятых на веру — ни одного, потому что все объявленные в дереве отношения реализованы. Два из восьми — моноиды минимума и максимума на типе вес, отрезке [0, +∞]: первые моноиды, появившиеся в корпусе .flang вообще. Моноида по сложению там нет намеренно — он не собирается, и язык предъявляет контрпример. Числа сверяются со сводом в flang/test/proof.test.mjs: проза не исполняется, значит сама не ломается.

Сторож меры — не единственное, что проверяется во время работы, и до 16 августа свод считал только его. Второй сторож — частичная встроенная форма: голова пустого списка, элемент за концом, к числу от строки, которая числом не является. Список таких форм закрыт и назван (ЧАСТИЧНЫЕ в flang/src/failures.mjs), а мест по ним втрое больше, чем у сторожа меры: 340 мест у 202 функций против 100 мест у 66. Число это мерено ИЗЪЯТИЕМ — свод считается со снятым анализом непустоты и с ним, — а не вспомнено.

Из этих мест 108 сняты, и сняты они уточнением типа, а не проверкой. У четырёх форм из восьми — голова, хвост, код символа, разделить — условие отказа одно и то же: «длина ноль». Значит и снимается оно одним уточнением, а не четырьмя частными случаями: список и строка носят нижнюю границу своей длины, ровно так же, как нат носит отрезок [0, 2^53−1]. Граница берётся из двух источников — из ПОСТРОЕНИЯ (добавить x к л на один длиннее л; литерал [1, 2, 3] длиной три; разделить даёт хотя бы один кусок всегда; голова строки в разборе — строка ровно из одного символа) и из СУЖЕНИЯ по условию (если пусто л то … иначе <здесь л непуст> — то же правило, каким сужаются числовые отрезки). Где длина доказанно не ноль, печать зовёт помощника без сторожа, и проверки во время работы там нет.

Стало: частичных форм в корпусе 264 мест у 184 функций. Тотальных, у которых во время работы не проверяется ничего, 4821 из 5034, было 2013. Мест снято 83, а функций прибавилось 33, и разница здесь не описка: функция переходит в чистые только когда снято ПОСЛЕДНЕЕ её место.

Остальные четыре формы не снимаются этим средством ни разу, и это названо, а не умолчано: элемент, символ и подстрока требуют ДВУСТОРОННЕЙ границы номера, а не непустоты, — это другой анализ; к числу частична неустранимо, потому что никакой тип строки не обещает, что она записывает число.

Это умеет и компилятор на самом flang, а не только эталон. Перенос сделан в flang/self/types.flang, и сверен он не по сообщениям — их непустота не меняет вовсе, — а ПО ОТМЕТКАМ: множество мест, признанных доказанными, обязано совпасть с эталонным поимённо, форма и место. На корпусе сверки совпали 240 мест из 240 (flang/test/self-types.test.mjs). До этого сверка была слепа к целому анализу: её 24 проверки оставались зелёными и при полном его отсутствии.

Свод называет и второе число, потому что «во время работы» читается про работу целиком: тотальная функция без единого места в своём теле, зовущая «Голова списка» из библиотеки, проверку во время работы всё равно встретит. Тотальных, у которых проверки нет ни в теле, ни у тех, кого они зовут, — 4043. Было 1737. Первое число говорит, чего стоит сама функция, второе — чего стоит её вызвать; подменять одно другим нельзя ни в какую сторону. Прибавка у второго числа больше (179 против 46) ровно потому, что снятое место в библиотеке делает чистыми всех, кто её зовёт.

Утверждение о поведении теперь можно высказать, и это новое. До слоя доказательства (flang/proof/SPEC.md) обычная функция flang не могла сказать о себе ничего: постусловие в AST было и работало, но поверхности у него не было вовсе — оно приходило только из свойства утилиты наследия FTS и от сторожа меры. Слово обеспечивает эту поверхность даёт, а теорема с утверждаем, индукция по, случай … то …, по свойству «…», по примеру «…», по предположению и следовательно доказано даёт доказательство — структурное, в духе Isar из Isabelle, а не скрипт из тактик. Тактик нет намеренно: тактика ищет, поиск нетотален, значит на flang её не написать, и жила бы она только в эталоне на JavaScript.

Доказательство проверяет ядро (flang/src/proofterm.mjs), и оно НИЧЕГО НЕ ИЩЕТ: каждый шаг обязан назвать факт, а ядро только сверяет. Принцип индукции при этом не заведён отдельным понятием — он читается с объявления суммы, потому что индуктивный тип есть начальная алгебра, и её универсальное свойство даёт сразу и свёртку (она в языке была с начала), и индукцию. Ядро сличает случаи с конструкторами: пропущенный конструктор — отказ.

Вся эта цепочка существует и на самом flang. У четырёх её слоёв есть близнецы, сверенные с эталоном побайтово: принцип (self/proof-initial.flang), сведение (self/proof-kernel.flang), связка постусловия с теоремой (self/obligations.flang) и свёртка терма в вердикт (self/proofterm.flang). Последние два — 138 функций против 1281 строки JavaScript — переносились с критерием «JSON.stringify знак в знак, до ключа и до порядка ключей», и расхождений у них ноль на 200 программах. Все восемь целей печати эти близнецы принимают: проверяльщик доказательств, живущий только в Node, был бы не частью языка, а частью среды.

Ведомость от этого получила четвёртое слово, и слова по-прежнему не взаимозаменяемы: «доказано» (терм принят ядром — утверждение обо ВСЕХ входах), «сетка N значений: нарушений не найдено», «объявлено, не доказано» (утверждение высказано, доказательства при нём нет — сюда попадает и старая форма теорема наследия FTS, которая разбирается, но следствий не даёт) и «на веру». Слова «проверено» в ведомости нет и не будет: оно и есть то, которое читается двумя способами.

Что доказано в дереве сегодня, числом: высказано 142 утверждения, из них 115 доказаны ядром — 19 индукцией по объявленной сумме, 3 индукцией по отрезку «нат», 1 индукцией по свёртке тела и 40 без теоремы, сведением цели с телом, — 26 идут сеткой примеров, 1 объявлено и не доказано.

Решающих правил у ядра три, и все три о ЧИСЛАХ: «не меньше 0», «не больше конечного литерала», «равно». Ко всему остальному приложен четвёртый ход, и он не правило: цель, в которой не осталось ни одного свободного имени, ВЫЧИСЛЯЕТСЯ. Ядро так уже поступало в одном месте — прогоняя пример, — и теперь поступает так везде, где имён не осталось: у утверждения без свободных имён значение ровно одно, и посчитать его значит ответить обо всём носителе. Отсюда берутся утверждения вида «таблица открывается оградой» или «окончания упорядочены от длинных к коротким»: правила для них нет и не предвидится, а счёт отвечает. Замкнутость при этом проверяется, а не предполагается, вычисление ограничено названным пределом и при исчерпании отказывает словами, а посчитанное «нет» ядро называет ложным утверждением, а не молчит. На корпусе дерева число доказанных от этого не изменилось: целей такого вида в нём пока нет.

Носителей у индукции два, и они не оттенки одного. По объявленной сумме принцип держится начальностью: часть значения меньше значения, и цепочка частей конечного дерева обрывается сама. По отрезку «нат» — конечностью [0, 2⁵³−1] и СТРОГИМ спуском на единицу, который ядро читает в теле функции. Без верхней границы второй принцип был бы ложным: «х минус 1 меньше х» в IEEE-754 неправда при х = 2⁵³+4, и ровно там же кончается «нат».

Все четыре числа сверяет со сводом flang/test/count-guard.test.mjs. До него тут стояли «4, 2, 1, 1» и обещание «сверяются тем же тестом», за которым не стояло ничего: flang/test/proof.test.mjs сверял семь других фраз этого файла, а эту — нет, и число утверждений успело вырасти с четырёх до девяти молча.

Второе число здесь важнее первого, и читать его надо с той стороны, с какой оно неприятно: 142 утверждения на 6585 функций. Машина доказательства работает, аксиом у неё ноль, подделку она отвергает — но зовут её почти нигде. Корпус на это обошли целиком, спрашивая у ядра про каждую функцию, сводится ли «результат не меньше 0» с её телом; «да» нашлось на десяти функциях из 2800. Семь из них долго нельзя было даже записать: они лежат в корпусе побайтовой неподвижной точки самоприменения, а слова обеспечивает не знал парсер на flang. С появлением продукции долг закрыт, и все семь утверждений стоят теперь у самих функций, а не в перенесённых копиях. Узкое место не в ядре: нат в корпусе стоит у полутора десятков параметров и ни у одного поля варианта, а тела функций с нат собраны из умножения, вызовов и длина — того, чего правило сведения не знает и знать не обязано.

С появлением индукции по отрезку это стало измеримым, а не предполагаемым. Корпус обойден принципом по числу: у 31 функции есть параметр нат, у 17 из них принцип ЧИТАЕТСЯ целиком — условие дна, ветвь базы и строгий спуск на месте, — и ни у одной обе посылки не сводятся сегодня. Упирается это не в индукцию: у шести («Факториал» на четырёх поверхностях, «Факториал» из stdlib/numbers и «Степень») дно сводится, а спуск стоит на УМНОЖЕНИИ, которого у правил сведения нет; у «Фибоначчи шагом» и «Ступени шагом» наоборот — спуск сводится допущением, а дно ложно, потому что накопитель объявлен число, и утверждение «результат не меньше 0» о них попросту неправда.

Граница ядра названа, а не обойдена. Рекурсивный случай ядро больше не отвергает: свести «высота хвоста неотрицательна» с «высота хвоста плюс 1 неотрицательна» — это правило сведения, доказанная теорема о IEEE-754, а не аксиома. Список аксиом ядра ПУСТ, и он остался пуст даже после того, как у языка появился точный тип нат, — вопреки тому, что здесь когда-то обещалось. нат дал не аксиомы, а ФАКТЫ ИЗ ПОДПИСИ: отрезок [0, 2⁵³−1] у объявленного имени ядро читает там, где автор его написал, и обе границы приезжают данными. Пуст список намеренно: числа flang — IEEE-754, где «х плюс 1 не меньше х» неправда при большом |х| (та же причина, по которой анализ ставит сторожа на постоянный шаг), а аксиома, которая иногда ложна, делает ложным всё, что из неё выведено. И границы у фактов разные: дно переживает сложение, потолок нет — сумма двух нат выходит за 2⁵³−1 законно, и утверждение об обратном ядро обязано отвергнуть.

Ядро, решающее всё это, теперь есть и на самом flang, и оно догнало эталон целиком. Раньше близнец был только у свёртки ПОМЕТОК шагов: кто расставил пометки — то есть кто решил, выведен шаг или нет, — оставалось на JavaScript. Теперь на flang написаны обе решающие половины: self/proof-initial.flang строит принцип индукции с объявления суммы, self/proof-kernel.flang сводит заключение к допущениям — все ТРИ решающих правила и все ЧЕТЫРЕ переписки нормализации, включая развёртку определений с названным пределом. Аксиом у близнеца ноль, и взять их ему неоткуда: он не объявляет ни одного факта, только читает данные ему.

Критерий верности тут строже, чем «оба согласились»: на каждом утверждении корпуса вердикт близнеца обязан совпасть с вердиктом эталона ТЕМ ЖЕ ПРАВИЛОМ, с ТЕМ ЖЕ ТЕКСТОМ причины и с тем же отчётом о развёрнутом — знак в знак. Сверено на 15 828 утверждениях, расхождений 0 (flang/test/self-proof-kernel.test.mjs). Подделка отвергается близнецом тем же правилом и тем же текстом, что эталоном.

Расширение доказуемого возможно и дальше: условия, укладывающиеся в линейную арифметику, разрешимы, и подключение решателя к условиям верификации остаётся открытой задачей. Обязательства для него уже есть и лежат данными (flang/src/obligations.mjs) — решателю останется их прочитать.

Эффекты выражаются описанием, а не выполняются. Язык чистый; работа с сетью или файлами — это построение описания действия, которое исполняет хозяин, среда, в которую напечатан модуль. Сделано: пять поручений (чтение и запись файла, запрос по сети, время, случайное число), объявление план, хозяин на Node и команда flang io. Функции, строящие поручения, проверяются обычными примерами и остаются тотальными — сеть в язык не входит. Монады ввода-вывода при этом нет: она требует параметрического полиморфизма, и вместо неё — машина продолжений (flang/cat/SPEC.md, «Чем это не монада»). Слой исполнения написан для одной цели из восьми.

См. также