Чего в языке пока нет: проверенный список

Список проверен на flang 0.7.29 — готовой сборке выпуска для Linux x86_64, 18 октября 2026 года. У каждого пункта стоит программа и ответ компилятора, снятый запуском, а не пересказ. Список недостач устаревает быстрее любой другой страницы о языке: когда недостачу закрывают, ни один тест не краснеет. Поэтому перед тем как полагаться на пункт, повторите его программу на своей версии — это минута.

Коды возврата, которые встретятся ниже: 0 — всё проверено, 1 — программа не прошла, 2 — неверный вызов команды, 3 — работа сделана, но доказано не всё, и недоказанное названо.

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

Всё это в прошлых версиях курса стояло в списке «нет». На 0.7.29 каждый пункт проверен запуском; программы короткие, их легко повторить.

Логические операции — одной строкой, с приоритетом или < и притом < не:

модуль «Логика»

тотальная функция «Допуск»
  принимает оплачен: признак, есть: признак, вручную: признак
  возвращает признак
  пример «оплачен и есть»
    дано оплачен равно да
    дано есть равно да
    дано вручную равно нет
    ожидается да
  пример «не оплачен, но вручную»
    дано оплачен равно нет
    дано есть равно нет
    дано вручную равно да
    ожидается да
  пример «ничего»
    дано оплачен равно нет
    дано есть равно да
    дано вручную равно нет
    ожидается нет
  (оплачен и притом есть) или (вручную и притом не оплачен)

Строка разбирается образцом так же, как список, и завершение такой рекурсии доказывается структурой — каждый виток получает часть строки:

модуль «Длина строки»

тотальная функция «Знаков»
  принимает текст: строка
  возвращает число
  пример «кот»
    дано текст равно "кот"
    ожидается 3
  разбор текст
    случай пусто
      то 0
    случай голова и хвост
      то 1 плюс «Знаков» от хвост

Мера убывания: что доказывается, а что проверяется при работе

Слово убывает называет параметр, который уменьшается на каждом рекурсивном вызове. Если параметр объявлен неотрицательное и уменьшается на единицу, компилятор это доказывает и проверок в работающую программу не вставляет:

модуль «Отсчёт»

тотальная функция «Сумма до»
  принимает н: неотрицательное
  возвращает число
  убывает н
  пример «до четырёх»
    дано н равно 4
    ожидается 10
  если н не больше 0
    то 0
    иначе н плюс «Сумма до» от (н минус 1)

$ flang check --proof sum-to.flang
…
чем несётся обещание «тотальная»:
  «Сумма до»  доказано точным шагом: аргумент 1 («н») объявлен натуральным и убывает на 1; …

Шаг, который мера не может уменьшить, отвергается до запуска. Задача Коллатца:

модуль «Коллатц»

тотальная функция «Шаги»
  принимает н: число
  возвращает число
  убывает н
  если н не больше 1
    то 0
    иначе если (н остаток от 2) равен 0
      то 1 плюс «Шаги» от (н делить на 2)
      иначе 1 плюс «Шаги» от (3 умножить на н плюс 1)

$ flang check collatz.flang
модуль «Коллатц»: функций 1, из них с доказанным завершением 0; типов 0
без доказанного завершения: «Шаги»
FLANG_NOT_TOTAL в файле collatz.flang, строка 11, столбец 20: тотальная функция «Шаги»: мера «н» на вызове «Шаги» не убывает — аргумент 3 умножить на «н» плюс 1 не меньше меры при любом её неотрицательном значении …
collatz.flang: не проверено — замечаний 1

Середина между этими случаями — алгоритм Евклида с мерой убывает б и шагом а остаток от б. Компилятор его принимает (код 0), но вывести спуск не может и говорит об этом прямо: спуск ядром не выведен — на веру: мера объявлена автором, … считает её при работе на каждом витке. То есть завершение здесь обеспечивает проверка во время работы: если мера не убыла, программа остановится с FLANG_MEASURE, а не зациклится.

Доказательства для всех входов

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

Алгебраические тождества над точными целыми — обе стороны раскрываются в многочлен и сравниваются (как тактика ring в Lean):

модуль «Кольцо»

утверждение «квадрат суммы»
  для всех а: точное целое и б: точное целое
  утверждаем ((а плюс б) умножить на (а плюс б)) равен ((а умножить на а) плюс (а умножить на б) плюс (б умножить на а) плюс (б умножить на б))

$ flang check --proof square-of-sum.flang
…
  утверждение «квадрат суммы» — доказано по объявленным типам аргументов: цель сведена правилом «кольцо точного целого» — утверждение обо ВСЕХ входах, а не о написанных; …
square-of-sum.flang: ПРОВЕРЕНО САМОСТОЯТЕЛЬНО — утверждений 1: доказано 1, … — код возврата 0

Подстановка доказанного — доказанное постусловие функции подставляется вместо её вызова в других доказательствах (как simp):

модуль «Подстановка»

тотальная функция «Приклеить пустое»
  принимает текст: строка
  возвращает строка
  обеспечивает «пустое не меняет» результат равен текст
  соединить текст с ""

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

$ flang check --proof rewrite.flang
…
  утверждений 2: доказано 2 (из них без теоремы 2), сетка 0, объявлено, не доказано 0

Законы моноида, функтора и естественного преобразования — объявление моноид порождает законы ассоциативности и единицы, и ядро доказывает их для всех значений носителя, если носитель — точное целое. В клоне репозитория flang check --proof flang/ct/yoneda-preorder.flang печатает законов утверждениями 9: доказано ядром 9, не доказано 0.

Перепроверка двумя программами. Ключ --record файл записывает само доказательство, и его независимо перепроверяют две программы: flang/proof/checker/checker.c на C и flang/proof/checker/second/ на Lean 4. Обе лежат в репозитории и собираются там же; на записи из примера выше обе отвечают согласием, а запись, исправленная руками хоть в одном знаке, отвергается:

$ make -C flang/proof/checker           # программа на C
$ make -C flang/proof/checker second    # программа на Lean 4 (нужен Lean из flang/proof/lean/lean-toolchain)
$ flang check --proof --record square-of-sum.record square-of-sum.flang
$ flang/proof/checker/сверщик square-of-sum.flang square-of-sum.record
ПРОВЕРЕНО — запись сошлась с исходником, и всё доказанное проиграно заново: утверждений 1, …
$ flang/proof/checker/second/out/второй-сверщик square-of-sum.flang square-of-sum.record
ПРОВЕРЕНО — утверждений 1, доказанных 1, блоки вывода приняты

Если передать путь к программе на C через FLANG_CHECKER, check --proof зовёт её сам и печатает независимо, сверщиком, проиграно 1 из 1 доказанных.

Чего нет в языке

Порядка на строках

меньше и больше работают только с числами:

модуль «Порядок строк»

тотальная функция «Раньше»
  принимает а: строка, б: строка
  возвращает признак
  пример «а раньше б»
    дано а равно "а"
    дано б равно "б"
    ожидается да
  а меньше б

$ flang check string-order.flang
FLANG_TYPE в файле string-order.flang, строка 10, столбец 3: левый операнд сравнения «lt» имеет тип строка: сравнения порядка допустимы только для чисел
…

Обход — функция «Строка раньше» из flang/stdlib/tree.flang: порядок написан на самом языке рекурсией по строкам.

Замены элемента по номеру и среза списка

Список читается по номеру (элемент N в …), но не правится: формы «список с заменённым N-м элементом» нет, как нет и среза «первые k». Значения в языке неизменяемы, и такая форма стоила бы копирования всего списка. Поэтому кучи и таблицы с обновлением на месте не пишутся.

модуль «Замена по номеру»

тотальная функция «Заменить второй»
  принимает элементы: список число
  возвращает список число
  заменить элемент 2 в элементы на 0

$ flang check replace-by-index.flang
FLANG_UNKNOWN_NAME в файле replace-by-index.flang, строка 6, столбец 3: имя «заменить» не связано: …

Изменяемого состояния и объектов с методами

Функция — отображение аргументов в результат; переменной, которую можно переписать, нет. Состояние, живущее между вызовами, передаётся аргументом и возвращается результатом либо живёт в процессе (процесс, глава «Синтаксис по факту»). Задачи вида «кэш с методами get/put» в их исходной постановке не выражаются.

Безымянных функций как значений

Значением бывает только именованная функция — функция «Удвоить». Стрелка х → … пишется только внутри встроенных форм (отобразить, отфильтровать, свёртка) и там видит параметры функции; вернуть её из функции нельзя:

модуль «Безымянная функция»

тотальная функция «Сделать прибавитель»
  принимает шаг: число
  возвращает функция из числа в число
  х → х плюс шаг

$ flang check closure.flang
FLANG_UNKNOWN_NAME в файле closure.flang, строка 6, столбец 3: имя «х» не связано: …

Разбора двух значений сразу

разбор сопоставляет одно значение. Пару приходится разбирать вложенными разбор:

модуль «Пара образцов»

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

$ flang check two-values.flang
FLANG_PARSE в файле two-values.flang, строка 6, столбец 12: у 'разбор' нет ни одного 'случай'

Перехвата отказа

Отказ встроенной формы — например, номер вне списка — останавливает вычисление, и поймать его нельзя. Ошибка, которую нужно обработать, описывается значением: тип «Результат» из flang/stdlib/result.flang с вариантами «Успех» и «Ошибка».

модуль «Отказ»

тотальная функция «Пятый»
  принимает элементы: список число
  возвращает число
  элемент 5 в элементы

тотальная функция «Пятый из двух»
  возвращает число
  «Пятый» от [1, 2]

$ flang run refusal.flang --function "Пятый из двух"
доказано: утверждений 0
FLANG_BUILTIN_ARGS: «элемент»: индекс 5 вне списка длиной 2
$ echo $?
1

flang check эту программу принимает: обещание тотальная значит «завершится или честно откажет», а не «не откажет никогда».

Сравнение 0 и −0 в примерах

Тип число использует IEEE-754 double. В 0.7.29 пример с произведением отрицательного числа на ноль отвергался, если ожидал 0, и оба значения в сообщении выглядели одинаково. В 0.7.32 этот пример проходит.

модуль «Минус ноль»

тотальная функция «Обнулить»
  принимает х: число
  возвращает число
  пример «минус три на ноль»
    дано х равно -3
    ожидается 0
  х умножить на 0

$ flang test negative-zero.flang
negative-zero.flang: примеров 1, прошло 1, не прошло 0

Внятной ошибки для варианта, названного ключевым словом

Варианты Плюс, Минус, Больше, Меньше, Да, Нет лексер читает как слова языка, и в образце случай Плюс они не разбираются. Работает явная форма случай вариант «Плюс», и сообщение её называет, но причину — совпадение имени со словом языка — не говорит:

модуль «Знак»

тип «Знак»
  вариант Плюс
  вариант Минус

тотальная функция «Множитель»
  принимает з: «Знак»
  возвращает число
  разбор з
    случай Плюс
      то 1
    случай Минус
      то -1

$ flang check keyword-variant.flang
FLANG_PARSE в файле keyword-variant.flang, строка 11, столбец 12: не разобрана конструкция: ожидался образец — в 'случай' годятся 'пусто', 'голова' и 'хвост', 'вариант «Имя»', …

Чего не доказывает ядро

Ядро не ищет доказательство, а применяет правила из закрытой таблицы (flang/proof/tables/inference-rules.tsv). Чего в таблице нет, то остаётся недоказанным, и отчёт это называет. Недоказанное утверждение не мешает flang check (код 0), но flang run откажется считать такую программу без ключа --на-веру (код 3).

Законов над число. Для double ассоциативность сложения ложна, и ядро её не доказывает — ни утверждением, ни законом моноида:

модуль «Кольцо на double»

утверждение «сочетательность сложения»
  для всех а: число и б: число и ц: число
  утверждаем ((а плюс б) плюс ц) равен (а плюс (б плюс ц))

$ flang check --proof double-associativity.flang
…
  утверждение «сочетательность сложения» — объявлено, не доказано: ни теоремы, ни примеров. …
double-associativity.flang: НЕ ПРОВЕРЕНО — утверждений 1: доказано 0, … объявлено, не доказано 1, … — код возврата 3

Тот же моноид сложения над точное целое доказывается целиком, а над число — только считается на нескольких значениях (законов утверждениями 6: доказано ядром 3, не доказано 3). Вещественных чисел ℝ в языке нет вовсе: перевод формулы с \mathbb{R} отвечает ℝ в flang нет: «число» — double IEEE-754, законы поля на нём ложны.

Законов монады. Объявление монада и форма в монаде есть, но три закона монады ядро не доказывает, а проверяет на конечном наборе значений. В клоне репозитория: flang check --proof flang/ct/monoid-and-monad.flang — законов утверждениями 8: доказано ядром 0, не доказано 8, код 3. То же у квадрата естественного преобразования в flang/ct/natural-square.flang: доказано ядром 0, не доказано 3.

Простых неравенств после ветвления. Постусловие «скидка не поднимает цену» верно на любых входах, но правила, которое свело бы его к ветвям тела, в таблице нет:

модуль «Скидка»

тотальная функция «К оплате»
  принимает цена: неотрицательное, скидка: неотрицательное
  возвращает число
  обеспечивает «скидка не поднимает цену» результат не больше цена
  пример «скидка меньше цены»
    дано цена равно 1000
    дано скидка равно 150
    ожидается 850
  пример «скидка больше цены»
    дано цена равно 100
    дано скидка равно 150
    ожидается 0
  если скидка не меньше цена
    то 0
    иначе цена минус скидка

$ flang run discount.flang --function "К оплате" --args '{"цена": 2500, "скидка": 400}'
не доказано: утверждений 1: доказано 0, сетка 1, на веру 0 — запуск только по явному согласию: --на-веру
…
$ flang run discount.flang --function "К оплате" --args '{"цена": 2500, "скидка": 400}' --на-веру
на веру: доказанность не считалась — запуск по ключу --на-веру
2100

Отчёт подсказывает два выхода: написать к утверждению теорема либо переписать условие так, чтобы оно совпало с ветвью тела.

Чего нет в готовой сборке

Архив выпуска (install.sh, Homebrew, deb, rpm) несёт двоичный файл, стандартную библиотеку и рантаймы целевых языков. Части инструментов в нём нет, они работают только в клоне репозитория:

• Программ перепроверки доказательств. check --proof в готовой сборке печатает НЕЗАВИСИМО НЕ ПРОВЕРЕНО — сверщика нет … все 1 доказанных стоят на слове ядра. Обе программы перепроверки собираются из репозитория, как показано выше.
• Английских сообщений. FLANG_LANG=en без каталога сообщений отвечает no message catalog was found … answering in Russian. С каталогом из клона (FLANG_MESSAGE_DIR=flang/messages) по-английски печатаются итоговые строки (verified — parsing, types, termination…), а текст большинства диагностик остаётся русским.
• Перевода формул. formula:read и formula:print — команды проекта из .flangrc репозитория; они зовут bootstrap/flang по пути внутри клона. В клоне со сборкой make -C bootstrap формула ∀ a ∈ ℤ, ∀ b ∈ ℤ, a + b = b + a превращается в утверждение flang и проверяется ядром, --latex принимает ту же формулу в LaTeX, а formula:print печатает утверждения файла обеими записями.
• Образца для flang new — см. дефекты ниже.

Известные дефекты 0.7.29

Это не решения языка, а ошибки; у каждой есть задача в репозитории.

• использует … только не подтягивает вспомогательные функции (#447). Строка использует «Dictionary» только «Положить», «Взять или запасное» даёт FLANG_UNKNOWN_NAME … неизвестная функция «Шаг взятия» и ещё 13 замечаний; без только тот же модуль подключается и проверяется.
• flang new в готовой сборке не создаёт пакет (#448): FLANG_NEW: не найден образец fspec/ … Пакет не создан, код 1.
• Функция без строки возвращает проходит проверку (#449): код 0, «замечаний нет».
• Служба flang --mcp-mode называет себя версией 0.6.0 (#450): в ответе initialize стоит "serverInfo":{"name":"flang","version":"0.6.0"}.
• flang run --args принимает только плоский объект скаляров. Список аргументом не передать: --args '{"элементы":[1,2]}' отвечает ждался плоский объект скаляров. Обход — функция без параметров, которая зовёт нужную с готовым списком, или пример внутри функции и flang test.
• HTTPS-ответ с Transfer-Encoding: chunked приходит неразобранным: тело ответа https://example.com/ начинается со строки длины куска 241.
• flang check --help устарел в разделе о категориях: справка говорит, что категорную поверхность бинарник «не судит вовсе», хотя на 0.7.29 законы моноида считаются и доказываются, а неверный изоморфизм даёт FLANG_ISO_NOT_INVERSE с контрпримером.

Чего нет вокруг языка

• Форматтера. flang fmt отвечает неизвестная команда «fmt», код 2. Линтер есть (flang lint: длина строк и глубина ветвлений по .flangrc), языковой сервер тоже (flang lsp). В репозитории языка, в docs/editors/, лежат клиент для VS Code, грамматика подсветки TextMate (scopeName: source.flang) и подсветка для Vim.
• Нативной сборки для Windows. Работает сборка для Linux под WSL.
• Сборки под именем flang без оговорок. Компилятор Fortran из LLVM тоже ставит команду flang; проверьте, что первой строкой flang --version печатает flang 0.7.29.
• Широкого круга пользователей. Известные программы на flang вне репозитория языка — flang-tui, flang-env, flang-ribbon и digitdisk, все из той же организации (страница «Библиотеки на flang»). Синтаксис на 0.x не заморожен; совместимость обещана только для формы JSON и кодов диагностик.

Как перепроверить

Каждую программу этой главы можно сохранить в файл и повторить:

$ flang check файл.flang        # разбор, типы, завершение, примеры
$ flang test файл.flang         # только примеры
$ flang check --proof файл.flang  # отчёт: что доказано и чем

Если пункт из раздела «нет» у вас проходит — значит, его уже сделали, и список устарел. Дальше — глава «Как читать репозиторий».