К README · Указатель документации

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

Что во flang сегодня не работает и что делать вместо этого. Полные списки — в docs/flang/SPEC.md §10 и в разделах «Долги» спецификаций.

Как читать отчёт о доказательствах

flang check --proof даёт каждому постусловию (обеспечивает) один из трёх результатов. Это разные вещи:

Завершение тотальная функций, типы и полнота pattern matching (разбор) всегда доказываются, а не тестируются.

Сверщик перепроверяет не каждое место доказательства: часть он берёт на слово ядра, называет в отчёте и отвечает кодом 3. 12 октября 2026 bootstrap/flang run-script checker:second на 634 записях проб и подделок насчитал 142 такие записи и 229 мест на слове ядра (до ADR-0103 — 144 и 232). Постусловие с таких что, снятым типом довода, сверщик переигрывает сам: step-by-restricted-postcondition-discharged.flang — код 0 у компилятора и у сверщика.

Чего доказать нельзя

Внешний SMT-решатель не подключён. Софт для медицины, авиации и космоса на flang не пишите: сертификация — это процесс, а не свойство языка (ADR-0031).

Язык

Записи в список по номеру нет. Читать элемент можно — элемент N в список, и это работает на всех целевых языках. Значения неизменяемы, поэтому «список с заменённым N-м элементом» — это новый список. Алгоритмы на изменяемой таблице — динамическое программирование вроде Coin Change или Edit Distance, хеш-таблица с корзинами — напрямую не переносятся. Для словаря берите готовый из библиотеки: список пар с линейным поиском (flang/stdlib/dictionary.flang), дерево поиска с поиском за O(log n) (flang/stdlib/tree.flang) или хеш-trie (HAMT), глубина которого ограничена длиной хеша (flang/stdlib/hashmap.flang).

Побитовых операторов нет. Берите функции библиотеки, которые делают то же арифметикой, например «Исключающее или байтов» (XOR байтов) в flang/stdlib/aes.flang.

Счёт вверх завершение не доказывает. Рекурсивный вызов на н плюс 1 отвергается с FLANG_NOT_TOTAL: «рекурсивный вызов не убывает». Переверните счёт вниз по параметру типа неотрицательное (неотрицательное целое) — тогда завершение доказывает сам тип (docs/examples/measure/natural.flang).

Когда шаг меняется от вызова к вызову, убывающую меру компилятор сам не находит. Он находит структурную рекурсию (по хвосту списка, по части дерева) и числовой аргумент, убывающий на постоянный шаг. Для остального напишите меру сами строкой убывает <выражение>: двоичный поиск — убывает верх минус низ плюс 1, алгоритм Евклида — убывает б (docs/examples/measure/). Сгенерированный код тогда проверяет во время работы, что мера целая, неотрицательная и строго убывает, и останавливается с FLANG_MEASURE, а не зависает. Та же проверка во время работы стоит при постоянном шаге по обычному число: числа — двойной точности IEEE-754, и x минус 1 равно x при больших x. Для параметра неотрицательное проверка не нужна и не генерируется: значение ограничено типом. Отчёт о доказательствах считает эти случаи: 70 функций завершаются постоянным шагом с проверкой во время работы, 67 — точным шагом без неё, а сама проверка стоит в 96 местах 84 функций.

Вариант с именем ключевого слова не сопоставляется. Если варианты называются Да, Нет, Плюс или Больше, случай Да читается как ключевое слово, и ошибка винит образец (FLANG_TYPE: образец-литерал имеет тип признак …), а не имя. Пишите случай вариант «Да» или переименуйте вариант.

Side effects — только через план. Функция сама файл не читает: она возвращает команду как данные (вариант «Прочитать файл» с путь равным …), flang io её выполняет и вызывает функцию снова с ответом. Команд 27, и список закрыт: чтение и запись файла текстом и байтами, удаление файла, временный каталог, список файлов каталога, HTTP-запрос, открытие и приём соединения, чтение и запись в соединение текстом и байтами, отправка и приём датаграммы, запуск процесса с вводом и без, показ на экран, ожидание события, размер экрана, текущее время, случайное число, случайные октеты, переменная среды, аргументы командной строки. Список — это функция «Варианты поручения» в flang/self/parser.flang, и постусловие там фиксирует его длину: 27. Неправильный UTF-8, прочитанный как текст, даёт FLANG_IO_NOT_TEXT; двоичные файлы читайте байтами.

https — своим клиентом, но после перепечатки семени. В исходниках рантайма «Запросить» по https исполняет клиент TLS 1.3 на языке (flang/stdlib/tls-client.flang), напечатанный в C и собранный в двоичный (ADR-0101). Двоичный из bootstrap/ получит его перепечаткой, а до неё зовёт curl. Клиент умеет только TLS_AES_128_GCM_SHA256, x25519, rsa_pss_rsae_sha256 и цепочку sha256WithRSAEncryption; узел без них — отказ FLANG_IO_TLS. Отзыв сертификата не проверяется. Корни — --trust-roots <файл PEM> или системная связка. Сырого TLS-сокета у плана нет: «Открыть соединение» — голый TCP. Датаграммы — только IPv4. Прогон 12 октября 2026 частной сборкой: ответ своего openssl s_server за 1,66 с против 0,015 с у curl (flang/proof/probes/network).

Программа с план генерируется в c, go, js, python, rust и ts (ADR-0100). cpp, csharp, elixir и java отказывают с FLANG_PLAN_UNSUPPORTED, называют план и не пишут ни одного файла. В c, go, python и rust план запускает прогонщик: flang_cli --plan <имя> [довод…]; его хозяин исполняет 9 родов поручений из 27 (файлы текстом и октетами, каталоги, среда, доводы), на сеть, процессы, часы, кости и экран отвечает «Сбой» с FLANG_IO_NOT_WIRED или FLANG_IO_NO_SCREEN. Такой план запускайте через flang io. Двоичный 0.7.25 печатает план в эти четыре цели только после перепечатки семени.

Компилятор отвечает по-английски не на всё. flang check при language = en в .flangrc (или FLANG_LANG=en) печатает рамку, итог и отчёт о доказательствах по-английски, а текст отказа — по каталогу flang/messages/catalog.tsv: английский шаблон есть у 13 кодов из 129 (bootstrap/flang run-script messages:check, 12 октября 2026). Отказ без шаблона и объяснение ядра после двоеточия печатаются по-русски; код FLANG_* один на всех языках. Справка, test, run, io и lint отвечают по-русски. Двоичный узнаёт каталог перепечаткой семени (ADR-0102).

Монады ввода-вывода нет. Шаги сцепляются так: функция возвращает команду и следующий шаг объявленным значением, а не скрытым замыканием. Чем это отличается от монады — в docs/ct/spec.md.

Правила арифметики вес, сотых и тысячных держатся не все. Над вес вычитание, умножение, деление веса на вес, остаток и проценты дают число: а минус б с возвращает вес — ошибка FLANG_TYPE («тело даёт число»), а с возвращает число проверка проходит, хотя спецификация обещает FLANG_INFINITY. Копейки с тысячными складываются без отказа FLANG_SCALE: сотых плюс тысячных при границах операндов проходит даже с возвращает сотых. Из 12 правил спецификации двоичный держит 7, не держит 4, одно не проверено (прогон 12 октября 2026, ADR-0099, задача 1747). Обход — объявлять результат тем же типом и не смешивать масштабы в одном выражении.

Примеры перед flang emit не прогоняются. Их прогоняют flang check и flang test; emit печатает и программу с ложным примером (задача 8397). Прогоняйте flang test <файл> перед печатью. Аргументы прогонщика напечатанной программы сверяют с объявленными типами исходники компилятора во всех десяти целях; двоичный 0.7.26 до печати семени впечатывает таблицу типов только в цель c и у вес не смотрит дно.

Категорные объявления

категория, морфизм, функтор, моноид, монада, изоморфизм, вложение, пересечение, свойство и естественные преобразования разбираются, но их правила двоичный компилятор проверяет лишь частично. У моноидов, монад, функторов, изоморфизмов, вложений, пересечений и объявленных свойств он не проверяет ни одного закона; у категорий и морфизмов не проверяет замкнутость под композицией, единицы и сходимость концов композиции. flang check называет, чего не проверил, и выходит с кодом 2:

$ flang check flang/ct/monoid-and-monad.flang
модуль «Monoid and monad»: функций 12, из них с доказанным завершением 12; типов 2
проверено НЕ ВСЁ: в программе объявлено то, чего бинарник не судит вовсе — monoids, monads. Ответ «замечаний нет» здесь читался бы как «проверено», а это неправда. Судья, вшитый в замыкание, до них не достаёт: `flang/self/setoid.flang` и `flang/self/setoid-oracle.flang` (264 функции) считают законы категорий, морфизмов и преобразований, и только их. Правил, которые сверяли бы названное выше, в замыкании этого двоичного нет ни строкой. Часть их в дереве написана слоями, которые сюда не ввезены, — а правило, которое никто не запускает, от ненаписанного неотличимо. Пока это так, названное выше не судит НИКТО
flang/ct/monoid-and-monad.flang: проверено НЕ ДО КОНЦА — разбор, типы, завершаемость, ядро и примеры прошли
$ echo $?
2

Функции внутри такого файла проверяются как обычно: типы, завершаемость, доказательства, unit-тесты. Если закон должен выполняться, запишите его как обеспечивает или пример у функций. Подробнее — в docs/ct/spec.md.

Процессы

Планировщик в сгенерированном C работает в двух режимах: один поток, который упорядочивает сообщения по seed, так что один seed даёт один и тот же журнал доставок, и пул рабочих потоков (поле workers в запросе). Пул быстрее только на программе с параллельной работой; на программе без неё он в разы медленнее. Замеры — в docs/scheduler-benchmark.md.