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

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

Доказано против проверено. Разница существенна, а слова звучат одинаково, поэтому:

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

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

Язык.

Функции первого класса есть в языке и печатаются во все восемь целей. Ограничение снято дефункционализацией (Reynolds, 1972): значение-функция — это тег, функция «Удвоить», а применение ф от 5 — диспетчер по конечному списку тегов, поэтому цели без замыканий и доказуемость завершения не страдают (flang/cat/HOF.md). Понижение делает ОДИН проход перед печатью (flang/src/defunc.mjs): бэкенду достаётся первопорядковая программа, и высшего порядка не видит ни один из восьми. Напечатанное собрано настоящими тулчейнами и сверено с интерпретатором на сетке входов. Чего пока нет — самоприменения: self/ новой формы не знает, поэтому программы репозитория (stdlib, examples) ею не пользуются.
Эффекты описываются, а не выполняются, и это работает: вариант «Прочитать файл» с путь равным … строит значение, а исполняет его хозяин (flang io, flang/src/host/node.mjs). Поручений пять — чтение и запись файла, запрос по сети, время, случайное число, — набор закрыт. Монады ввода-вывода при этом НЕТ, и причина уже не в полиморфизме: параметрические типы есть и в языке, и в самоприменении, и в стандартной библиотеке («Возможно» от «А» в flang/stdlib/optional.flang). Не хватает теоркат-слоя: checkFunctors знает имя типа, а не его применение, — фаза 3 в flang/cat/POLY.md. Пока её нет, последовательность действий выражается машиной продолжений, где продолжение объявлено значением, а не спрятано в замыкании; чем это отличается от монады — flang/cat/SPEC.md, раздел «Эффекты и HTTP». Слой исполнения сделан для одной цели из восьми (Node); печать программы с планом — во всех восьми.
Массив читается по номеру за постоянное время (элемент N в СПИСОК, семь целей из восьми), а словарь есть трёх видов: список пар с линейным поиском (dictionary.flang), дерево поиска с приоритетом по хешу ключа за O(log n) (tree.flang) и дерево по цифрам хеша за ПОСТОЯННОЕ время (hashmap.flang, HAMT: глубина ограничена четырнадцатью цифрами хеша при любом числе ключей). Чего нет — ЗАПИСИ по номеру: значения неизменяемы, и «список с заменённым N-м» пришлось бы собирать целиком. Пока её нет, не переносится табличное динамическое программирование (Coin Change, Edit Distance) и не строится хеш-таблица КОРЗИНАМИ — та, которой нужен массив с заменой по номеру; словарь с постоянным доступом при этом строится, потому что дерево переписывает только путь к ключу, а не весь массив. Побитовых операций тоже нет.
Анализ тотальности ВЫВОДИТ структурное убывание и числовую меру с ПОСТОЯННЫМ шагом — литералом (н минус 1) или параметром, приезжающим в вызов неизменным и строго больше нуля (н минус ш при если ш не больше 0). Там, где шаг МЕНЯЕТСЯ от витка к витку, вывести его нечем, и меру НАЗЫВАЕТ автор — строкой убывает <выражение>. Этим пишутся двоичный поиск (убывает верх минус низ плюс 1), Евклид (убывает б) и счёт вверх (убывает предел минус н); список-«топливо» им больше не нужен — примеры в flang/examples/measure/. Убывания с дном для доказательства мало: 1, ½, ¼ … больше нуля всегда, поэтому сторож объявленной меры проверяет три вещи сразу — строгое убывание, неотрицательность и ЦЕЛОСТЬ. Мера с постоянным шагом подпёрта тем же сторожем по другой причине: числа flang — IEEE-754 double, и при большом |x| x минус 1 равен x. Не убыло — отказ FLANG_MEASURE, одинаковый у вычислителя и у всех восьми целей, а не зацикливание.
Сторож с постоянного шага СНИМАЕТСЯ, если параметр объявлен точным натуральным (нат — целое из [0, 2^53−1]). Тип даёт рассуждению оба конца, которых не хватало: дно 0 и потолок, ниже которого н минус c при целом c ≥ 1 ТОЧНО меньше н. Доказательство становится полным, и ведомость называет пятый носитель обещания — «точным шагом», единственный без сторожа. Мерено на корпусе: 16 функций несли обещание постоянным шагом со сторожем, осталось 2; мест сторожа 100 вместо 115, добавлено НОЛЬ — переполнение ловится расширением типа (нат плюс нат это число), а не проверкой в напечатанном коде. Образец — [flang/examples/measure/natural.flang](../../flang/examples/measure/natural.flang).
Вариант, названный ключевым словом (Да, Плюс, Больше), в образцах не разбирается, и диагностика винит образец вместо настоящей причины. Обходится переименованием либо явной формой случай вариант «Имя», которой пользуется стандартная библиотека.

Категорная поверхность. Морфизмы, композиция, цепочки, единицы, функторы, бифункторы, изоморфизмы, моноиды, группы и монады реализованы; у монады есть форма связывания в монаде. Отношения множеств сказаны двумя словами: вложение — подобъект (стрелка, которая ничего не склеивает), пересечение — расслоенное произведение над объемлющим множеством. Устройство обоих доказывается сличением объявлений, инъективность вложения проверяется на значениях автора и при склейке предъявляет контрпример, а непустота общей части подтверждается свидетелем; универсальность общей части остаётся допущением, и следствий из неё компилятор не выводит ([flang/cat/SETS.md](../../flang/cat/SETS.md)). Объединение словом НЕ стало: ко-произведение в языке уже есть — это тип … вариант … с исчерпывающим разбором. Стрелка вправе нести закон: даёт называет функцию, закон — примеры, и нарушенный закон валит flang test, называя и стрелку, и закон. Обратимость изоморфизма проверяется там, где обе стрелки названы через даёт, и остаётся допущением автора там, где хотя бы одна — нет. Предусловие (требует) не заведено: оно есть в контракте как задуманное, не как сделанное. Не реализованы естественные преобразования — они описаны в [flang/cat/SPEC.md](../../flang/cat/SPEC.md). Имена категорий в объявлении функтора — пометка для читателя, а не проверяемое утверждение. Монадой сегодня не объявить список и всё рекурсивное, включая ввод-вывод: отображение эндофунктора печатается на месте, поэтому параметр обязан стоять в поле целиком ([flang/cat/MONAD.md](../../flang/cat/MONAD.md)).

Конкурентность. Сделаны все семь шагов, но шестой — наполовину. Планировщик в рантайме C проверочный: один поток и чередование по семени, побайтово сходящееся с эталоном; рабочего пула потоков нет, и цена его измерена на двух машинах (передача пробега другому потоку стоит от четырёх до четырнадцати пробегов, смотря по машине). Процессы печатаются только в Elixir и C, а остальные шесть целей дают из программы с процесс обработчики как обычные функции и больше ничего. породить заводит экземпляры объявленных видов на ходу — в эталоне и в цели C, но не на BEAM, — и имя порождённому даёт родитель, потому что описанное действие не может вернуть ничего; адресат сообщения по-прежнему обязан быть литералом, поэтому говорить с порождённым можно только тем, с чем он родился; распределённости нет. Сетка семян проверяет конечный набор чередований — это проверенное утверждение, а не доказанное, и свободы от взаимной блокировки она не даёт. Измерение сделано на занятой машине (средняя нагрузка 18–76 при восьми доступных ядрах), поэтому числа времени в нём — верхние оценки, и рядом с каждым названа нагрузка; числа, от неё не зависящие (витки, редукции, байты), названы отдельно и повторяются от прогона к прогону.