Известные ограничения

Названы прямо, потому что на проект с необозначенными границами нельзя опереться. Та же граница проведена в docs/overview.ru.md; полные списки — в flang/SPEC.md §10 и в разделах «Долги» контрактов.

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

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

Три слова — не украшение прозы: ровно ими отвечает отчёт о доказательствах (flang check --proof) и служба для помощника, и эта страница одно вместо другого не употребляет.

Расширение доказуемого возможно — условия, укладывающиеся в линейную арифметику, разрешимы, — но подключение решателя к условиям верификации остаётся открытой задачей, а не готовой возможностью.

Язык.

Функции первого класса есть в языке и печатаются во все восемь целей. Ограничение снято дефункционализацией (Reynolds, 1972): значение-функция — это тег, функция «Удвоить», а применение ф от 5 — диспетчер по конечному списку тегов, поэтому цели без замыканий и доказуемость завершения не страдают (flang/cat/HOF.md). Понижение делает ОДИН проход перед печатью (flang/self/defunc.flang): бэкенду достаётся первопорядковая программа, и высшего порядка не видит ни один из восьми. Напечатанное собрано настоящими тулчейнами и сверено с интерпретатором на сетке входов. Чего пока нет — самоприменения: self/ новой формы не знает, поэтому программы репозитория (stdlib, examples) ею не пользуются.
Эффекты описываются, а не выполняются, и это работает: вариант «Прочитать файл» с путь равным … строит значение, а исполняет его тот, кто запустил план (flang io). Поручений двадцать, и набор закрыт: чтение и запись файла знаками и отдельно октетами, удаление файла, заведение временного каталога, перечисление каталога, запрос по сети, открытие и приём соединения, чтение и запись в соединение знаками и отдельно октетами, запуск процесса и запуск процесса с вводом, показ на экран, ожидание события, текущее время, случайное число. Список закрыт не на словах: он лежит одной строкой в функции «Варианты поручения» (flang/self/parser.flang), и её длину — 20 — держит обеспечивает, то есть проверяет компилятор. Октетная пара у файла заведена 22 августа 2026: до неё двоичный файл проходил сквозь текстовую МОЛЧА — 4096 октетов на входе, 7 байт на выходе. Теперь текстовая пара на неправильном UTF-8 отказывает (FLANG_IO_NOT_TEXT), а октетная возит двоичный байт в байт. Монады ввода-вывода при этом НЕТ, и причина уже не в полиморфизме: параметрические типы есть и в языке, и в самоприменении, и в стандартной библиотеке («Возможно» от «А» в flang/stdlib/optional.flang). Не хватает теоркат-слоя: проверка функторов знает имя типа, а не его применение, — фаза 3 в flang/cat/POLY.md. Пока её нет, последовательность действий выражается машиной продолжений, где продолжение объявлено значением, а не спрятано в замыкании; чем это отличается от монады — flang/cat/SPEC.md, раздел «Эффекты и HTTP». Печать программы с объявлением план работает у ОДНОЙ цели из восьми: js печатает объявление целиком и возвращает 0, а остальные семь отказывают кодом FLANG_PLAN_UNSUPPORTED, называют план по имени и не пишут ни файла (текст отказа — flang/self/bootstrap/compiler.flang). До 22 августа 2026 те же семь печатали программу кодом 0 и объявление при этом молча теряли — худший из исходов, потому что модуль собирался и не работал. Разбор — docs/zettel/pechat-plana-obeshchana-naiznanku-i-sverit-eyo-nechem.md.
Массив читается по номеру за постоянное время (элемент N в СПИСОК, семь целей из восьми), а словарь есть трёх видов: список пар с линейным поиском (dictionary.flang), дерево поиска с приоритетом по хешу ключа за O(log n) (tree.flang) и дерево по цифрам хеша за ПОСТОЯННОЕ время (hashmap.flang, HAMT: глубина ограничена четырнадцатью цифрами хеша при любом числе ключей). Чего нет — ЗАПИСИ по номеру: значения неизменяемы, и «список с заменённым N-м» пришлось бы собирать целиком. Пока её нет, не переносится табличное динамическое программирование (Coin Change, Edit Distance) и не строится хеш-таблица КОРЗИНАМИ — та, которой нужен массив с заменой по номеру; словарь с постоянным доступом при этом строится, потому что дерево переписывает только путь к ключу, а не весь массив. Побитовых операций тоже нет.
Анализ тотальности ВЫВОДИТ структурное убывание и числовую меру с ПОСТОЯННЫМ шагом — литералом (н минус 1) или параметром, приезжающим в вызов неизменным и строго больше нуля (н минус ш при если ш не больше 0). Там, где шаг МЕНЯЕТСЯ от витка к витку, вывести его нечем, и меру НАЗЫВАЕТ автор — строкой убывает <выражение>. Этим пишутся двоичный поиск (убывает верх минус низ плюс 1) и Евклид (убывает б); список-«топливо» им больше не нужен — примеры в examples/measure/. Счёт ВВЕРХ мерой не пишется: верхней границы у него нет, и доказывать нечем — его переворачивают в счёт вниз по параметру типа неотрицательное, и тогда доказывает сам тип (examples/measure/natural.flang). Убывания с дном для доказательства мало: 1, ½, ¼ … больше нуля всегда, поэтому сторож объявленной меры проверяет три вещи сразу — строгое убывание, неотрицательность и ЦЕЛОСТЬ. Мера с постоянным шагом подпёрта тем же сторожем по другой причине: числа flang — IEEE-754 double, и при большом |x| x минус 1 равен x. Не убыло — отказ FLANG_MEASURE, одинаковый у вычислителя и у всех восьми целей, а не зацикливание.
Сторож с постоянного шага СНИМАЕТСЯ, если параметр объявлен точным натуральным (неотрицательное — целое из [0, 2^53−1]). Тип даёт рассуждению оба конца, которых не хватало: дно 0 и потолок, ниже которого н минус c при целом c ≥ 1 ТОЧНО меньше н. Доказательство становится полным, и ведомость называет пятый носитель обещания — «точным шагом», единственный без сторожа. Числа берутся из ведомости и подставляются сборкой, а не набираются: сегодня обещание несут постоянным шагом со сторожем 43 функций, точным шагом без сторожа — 30, а сторож стоит в 145 местах у 107 функций. Добавлено при переходе на неотрицательное НОЛЬ мест — переполнение ловится расширением типа (неотрицательное плюс неотрицательное это число), а не проверкой в напечатанном коде. Образец — examples/measure/natural.flang.
Вариант, названный ключевым словом (Да, Плюс, Больше), в образцах не разбирается, и диагностика винит образец вместо настоящей причины. Обходится переименованием либо явной формой случай вариант «Имя», которой пользуется стандартная библиотека.

Категорная поверхность. Морфизмы, композиция, цепочки, единицы, функторы, бифункторы, изоморфизмы, моноиды, группы и монады реализованы; у монады есть форма связывания в монаде. Отношения множеств сказаны двумя словами: вложение — подобъект (стрелка, которая ничего не склеивает), пересечение — расслоенное произведение над объемлющим множеством. Устройство обоих доказывается сличением объявлений, инъективность вложения проверяется на значениях автора и при склейке предъявляет контрпример, а непустота общей части подтверждается свидетелем; универсальность общей части остаётся допущением, и следствий из неё компилятор не выводит (flang/cat/SETS.md). Объединение словом НЕ стало: ко-произведение в языке уже есть — это тип … вариант … с исчерпывающим разбором. Стрелка вправе нести закон: даёт называет функцию, закон — примеры, и нарушенный закон валит flang test, называя и стрелку, и закон. Обратимость изоморфизма проверяется там, где обе стрелки названы через даёт, и остаётся допущением автора там, где хотя бы одна — нет. Предусловие (требует) реализовано, и снимает его вызывающий, как в Dafny: внутри тела это известный факт, от которого рассуждает ядро; у каждого вызова — обязательство, отвергаемое по имени (FLANG_PRECONDITION_CALL); на границе программы (--args, примеры) оно вычисляется, потому что доказывать там не из чего. В тело функции проверка не печатается ни у одной цели, и цена названа байтами: программа без единого требует печатается байт в байт как прежде, программа с одним растёт ровно на дверь — 334 байта у Python, 349 у Java, 369 у Elixir, 387 у C#, 452 у Rust, 462 у Go, 477 у C и 1 654 у JavaScript (flang/SPEC.md, «Предусловия функции»). Не реализованы естественные преобразования — они описаны в flang/cat/SPEC.md. Имена категорий в объявлении функтора — пометка для читателя, а не проверяемое утверждение. Монадой сегодня не объявить список и всё рекурсивное, включая ввод-вывод: отображение эндофунктора печатается на месте, поэтому параметр обязан стоять в поле целиком (flang/cat/MONAD.md).

Конкурентность. Планировщик в рантайме C работает в двух режимах. Проверочный — один поток и чередование по семени: он даёт побайтово тот же журнал доставок, что свидетель, и ради этого он и нужен. Второй — пул потоков, он включается полем workers в запросе и измерен прямо: на программе с параллельной работой пул быстрее в 1,85–4,80 раза уже при одном пробеге на передачу, а на программе БЕЗ параллелизма медленнее в 6,7 раза и жжёт при этом пятнадцать ядер (замеры — docs/scheduler-benchmark.md). Процессы печатают ТРИ цели — C, Elixir и JavaScript; остальные пять (Go, Rust, Python, Java, C#) программу с процесс печатать ОТКАЗЫВАЮТСЯ кодом FLANG_CONC_UNSUPPORTED, а не печатают её половину. породить заводит экземпляры объявленных видов на ходу у свидетеля и у цели C; планировщики JavaScript и Elixir отвечают на это действие названной ошибкой. Имя порождённому даёт родитель, потому что описанное действие не может вернуть ничего; адресат сообщения по-прежнему обязан быть литералом, поэтому говорить с порождённым можно только тем, с чем он родился; распределённости нет. Сетка семян проверяет конечный набор чередований — это проверенное утверждение, а не доказанное, и свободы от взаимной блокировки она не даёт. Свободной машины при замерах не было ни разу (нагрузка 125–734 при 256 ядрах, на замерах пула 60–1250), поэтому все числа времени в них — верхние оценки; числа, от нагрузки не зависящие (витки, редукции, байты), названы отдельно и повторяются от прогона к прогону.