flang компилятор доказывает, что программа не зациклится 0.6.2 GitHub English

Служба flang для ИИ-помощника

flang --mcp-mode — служба MCP: JSON-RPC по стандартным потокам, по сообщению на строку. Её запускает помощник, а не человек: запущенная руками, она молча ждёт строк — это не зависание.

Всё на этой странице снято прогоном 24 августа 2026 на flang 0.6.2. Рядом с каждым числом и каждой цитатой стоит команда, которая их даёт; ответы приведены дословно — в том числе там, где служба ведёт себя не так, как ожидаешь.

Проверить за полминуты

printf '%s\n' '{"jsonrpc":"2.0","id":1,"method":"initialize","params":{}}' | flang --mcp-mode
{"jsonrpc":"2.0","id":1,"result":{"protocolVersion":"2025-06-18","capabilities":{"tools":{}},"serverInfo":{"name":"flang","version":"0.6.0"}}}

serverInfo.version — не версия двоичного. Строка "0.6.0" вписана прямо в flang/self/mcp.flang и за выпусками не следует. Двоичный, давший ответ выше, на прямой вопрос отвечает иначе:

flang --version
flang 0.6.2

Узнавать по ответу службы, какой двоичный отвечает, поэтому нельзя.

Как подключить

{"mcpServers": {"flang": {"command": "flang", "args": ["--mcp-mode"], "env": {}}}}

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

Средства: ровно два

printf '%s\n' '{"jsonrpc":"2.0","id":1,"method":"initialize","params":{}}' \
              '{"jsonrpc":"2.0","id":2,"method":"tools/list","params":{}}' \
  | flang --mcp-mode | tail -1 | python3 -m json.tool
СредствоОбязательные поляЧто возвращает
flang_checksourceотчёт по всей программе целиком
flang_provesource, claimчем несётся ОДНО названное обещание

claim — имя из строки обеспечивает «имя» цель, а не текст самой цели. Имя, в программе не найденное, отказом не считается и разбирается отдельной строкой: Обещания «…» в программе нет.

В ответе одно текстовое поле — ни «ок», ни isError

Помощнику неоткуда взять зелёную галочку: её нет в протоколе. У result один ключ, у элемента content — два:

printf '%s\n' '{"jsonrpc":"2.0","id":1,"method":"initialize","params":{}}' \
  '{"jsonrpc":"2.0","id":2,"method":"tools/call","params":{"name":"flang_check","arguments":{"source":"модуль «П»\n"}}}' \
  | flang --mcp-mode | tail -1 \
  | python3 -c 'import json,sys; d=json.load(sys.stdin); print(list(d["result"]), list(d["result"]["content"][0]))'
['content'] ['type', 'text']

Значит, ветвиться придётся по тексту. Ветвитесь по ПЕРВОЙ СТРОКЕ — у каждого исхода она своя и дословно такая:

Первая строка ответаЧто произошло
Слова ведомости, и они НЕ взаимозаменяемы:проверка прошла, дальше идёт отчёт
Программа НЕ ПРОШЛА проверку языка, и ведомость доказательства поэтому не печатается.ответ flang_check: программа отвергнута, отчёта не будет
Программа НЕ ПРОШЛА проверку языка, доказывать нечего:то же в ответе flang_prove
Обещания «…» в программе нет.имя в claim не найдено; программа при этом цела

Ниже первой строки идут строки вида FLANG_КОД, строка N, столбец M: …. Ветвиться по словам «не прошла» слишком грубо: под этой строкой лежат опечатка разбора, несовпадение типов, не сошедшийся пример и ненайденный файл — четыре разных дела с четырьмя разными починками. Различает их только код.

Ошибки протокола

printf '%s\n' '{"jsonrpc":"2.0","id":1,"method":"initialize","params":{}}' \
  '{"jsonrpc":"2.0","id":2,"method":"resources/list","params":{}}' \
  'это не json' \
  '{"jsonrpc":"2.0","id":4,"method":"tools/call","params":{"name":"flang_check","arguments":{}}}' \
  '{"jsonrpc":"2.0","id":5,"method":"tools/call","params":{"name":"flang_nonexistent","arguments":{}}}' \
  | flang --mcp-mode

Пять строк на входе — четыре ответа на выходе:

{"jsonrpc":"2.0","id":2,"error":{"code":-32601,"message":"служба flang не знает метода «resources/list»"}}
{"jsonrpc":"2.0","id":4,"error":{"code":-32602,"message":"в запросе нет поля «source» — текста программы на flang"}}
{"jsonrpc":"2.0","id":5,"error":{"code":-32602,"message":"служба flang не знает средства «flang_nonexistent». Их два: flang_check и flang_prove"}}

Строка, не разобравшаяся как JSON, ответа в потоке не получает вовсе — ни ошибки, ни пустого объекта. Служба говорит о ней, но в ДРУГОЙ поток:

flang --mcp-mode: строка не разобрана как JSON, пропущена

Это стандартный поток ошибок, и большинство клиентов MCP его выбрасывает. Значит, помощник, ждущий ответ на каждый запрос, встанет здесь навсегда и не узнает почему. Ставьте срок ожидания и подбирайте этот поток.

Пять слов отчёта — и шестое, которого нет в словаре

Словарь едет в каждом успешном ответе, дословно и целиком: помнить его между вызовами не нужно.

Слова ведомости, и они НЕ взаимозаменяемы:
  «доказано» — утверждение обо ВСЕХ входах, выведенное из объявлений и структуры;
  «доказано индукцией по «Т»» — то же обо всех входах типа «Т»;
  «сетка N» — посчитано на N значениях автора. ЭТО НЕ ДОКАЗАТЕЛЬСТВО;
  «объявлено, не доказано» — утверждение высказано, доказательства при нём нет;
  «НАРУШЕНО» — ложь, уже найденная примером автора.
Ни одно из этих слов не сводится к «ок».

Ниже словаря, в самом отчёте, встречается шестое слово — на веру («не посчитано ничем, допущение автора»). В присылаемый словарь оно не входит: помощник, разбирающий ответ по пяти словам, на нём споткнётся.

Последние строки отчёта считают исходы числом. Вот они с настоящего модуля — examples/crypto/certificate.flang, разбор сертификата X.509 на 121 функцию:

итог:
  функций 121: тотальных 121, обычных 0
  обещание несёт: композиция 120, структура 0, точный шаг 0, постоянный шаг 1, объявленная мера 0
  сторожей в рантайме: 1 место
  законов на сетке: 0 (значений в сетках 0); на веру: 0
  утверждений 292: доказано 174 (из них индукцией 25) (из них без теоремы 139, объявленным типом 1), сетка 118, объявлено, не доказано 0 (шагов в термах 11)

По этим числам помощник видит не то, что доказано, а чего он не знает: из 292 утверждений 118 стоят на значениях автора, а не на доказательстве. Слово «проверено» такой разницы не передаёт, и потому его в ответе нет.

Отказ дороже доказательства

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

модуль «Срок»

тотальная функция «Дней осталось»
  принимает выдан: число, ныне: число
  возвращает число
  обеспечивает «срок никогда не отрицателен» результат не меньше 0
  пример «просрочен»
    дано выдан равно 10
    дано ныне равно 400
    ожидается -25
  (выдан плюс 365) минус ныне
python3 -c 'import json; print(json.dumps({"jsonrpc":"2.0","id":1,"method":"initialize","params":{}}))' > zapros.jsonl
python3 -c 'import json; print(json.dumps({"jsonrpc":"2.0","id":2,"method":"tools/call","params":{"name":"flang_prove","arguments":{"source":open("srok.flang").read(),"claim":"срок никогда не отрицателен"}}},ensure_ascii=False))' >> zapros.jsonl
flang --mcp-mode < zapros.jsonl | tail -1 \
  | python3 -c 'import json,sys; print(json.load(sys.stdin)["result"]["content"][0]["text"])'
Программа НЕ ПРОШЛА проверку языка, доказывать нечего:

FLANG_BOUND_ON_NAN, строка 6, столбец 3: постусловие «срок никогда не
отрицателен» функции «Дней осталось» ЛОЖНО, и контрпример назван: «выдан»
объявлен типом «число», а «не число» живёт в этом типе и стоит ВНЕ ПОРЯДКА —
оно не больше и не меньше ничего, включая самоё себя. […] Позовите «Дней
осталось» от (0 делить на 0) — рантайм ответит FLANG_PROPERTY. Чинится тремя
способами: объявить вход отрезком («нат», «целое») […]; поставить предусловие
[…]; либо оговорить границу […]

Контрпример назван не тот, что писал автор. Автор видел просрочку и написал -25; служба показала вход, о котором автор не думал вовсе. Вот чего помощник от себя не получит: он написал обещание, будучи в нём уверен, — и узнал, что оно ложно, до первого запуска, а не после.

Обратный случай — обещание не ложно, но и не доказано. Ответ говорит и это, и что с обещанием будет дальше:

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

Что ловится за один прогон, а что нет

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

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

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

тотальная функция «Заголовок»
  принимает имя: строка
  возвращает число
  имя плюс 1

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

Ошибка разбора приходит одна и глушит остальные. flang check chetyre.flang:

chetyre.flang: не проверено — замечаний 1
FLANG_PARSE в файле chetyre.flang, строка 6, столбец 10: не разобрана
конструкция: неожиданное 'список' — это слово занято языком, именем оно быть не
может: напишите имя в ёлочках («список») или переименуйте; а если слово попало в
форму лишним — уберите его

Ни одна ошибка типов из того же файла не названа — их ещё не искали.

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

модуль «Отчёт»: функций 3, из них с доказанным завершением 3; типов 0
chetyre-2.flang: не проверено — замечаний 2
FLANG_TYPE в файле chetyre-2.flang, строка 15, столбец 3: левый операнд «add»: ожидался число, получен строка
FLANG_TYPE в файле chetyre-2.flang, строка 20, столбец 3: функция «Метка» объявлена как строка, а тело даёт число

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

модуль «Отчёт»: функций 3, из них с доказанным завершением 3; типов 0
chetyre-3.flang: проверено — разбор, типы, завершаемость, ядро и примеры; замечаний нет

Ошибку такого рода служба ловит ровно тогда, когда автор написал при функции обещание или пример. Одна вписанная строка ожидается 3 меняет ответ:

chetyre-4.flang: не проверено — замечаний 1
FLANG_EXAMPLE: пример «три строки» функции «Строк в списке»: значение не
совпало с ожидаемым: ожидалось 3, получено 0

То есть три ошибки из четырёх компилятор нашёл сам и до запуска — но за два прогона, а не за один. Четвёртую он нашёл тоже, но лишь после того, как автор сказал, чего ждёт.

Служба не видит соседних файлов

Самая дорогая ошибка при подключении. Служба получает source — текст, и только текст. Файла у неё нет, а строка ввоза в тексте есть:

модуль «Сертификат»
  использует «X.509» из "../../flang/stdlib/x509.flang"

Относительный путь служба считает от СВОЕГО рабочего каталога. Тот же файл, который flang check с диска проверяет без замечаний, через службу отвечает так:

FLANG_IMPORT_NOT_FOUND, строка 1, столбец 1: не найден модуль «X.509»:
/srv/flang/stdlib/x509.flang (ENOENT: no such file or directory)
FLANG_UNKNOWN_NAME, строка 68, столбец 31: неизвестная функция «Версия сертификата»
…

Одна ненайденная строка ввоза дала 41 замечание: 1 FLANG_IMPORT_NOT_FOUND, 27 FLANG_UNKNOWN_NAME и 13 FLANG_NOT_TOTAL. Считаются они так (в zapros.jsonl здесь и ниже лежит initialize и tools/call со средством flang_check, где source — текст certificate.flang целиком):

flang --mcp-mode < zapros.jsonl | tail -1 | python3 -c \
 'import json,sys,re,collections; t=json.load(sys.stdin)["result"]["content"][0]["text"]; print(collections.Counter(re.findall(r"FLANG_[A-Z_]+", t)))'

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

cd examples/crypto && flang --mcp-mode < zapros.jsonl | tail -1

Лечится, стало быть, двумя способами: запускать службу с рабочим каталогом проекта либо слать программу одним текстом, без ввозов.

Сколько это стоит

Замер: flang check под /usr/bin/time, по десять прогонов, машина общая.

Что проверяемРазмерВремя
одна функция с обещанием и примером12 строк, 1 функция0,03 с
examples/leetcode/001-two-sum.flang65 строк, 3 функции0,12 с
examples/crypto/certificate.flang с ввозами121 функция, 5 файлов92 с
/usr/bin/time -f '%e с' flang check examples/leetcode/001-two-sum.flang
/usr/bin/time -f '%e с' flang check examples/crypto/certificate.flang

Тот же расчёт скриптом на Python — 0,01 с; из каждой строки таблицы 0,01 с приходится на сам запуск. Обмен по MCP поверх проверки добавляет 0,004 с: initialize плюс tools/call на программе из первой строки — 0,036 с целиком.

Читается таблица так: на скрипте доказательство бесплатно — разница с обычным запуском в сотые доли секунды, и звать службу можно на каждую правку. На настоящем модуле оно стоит полторы минуты, то есть один вызов на просмотр, а не на нажатие клавиши.

Второй расход — не время, а место в разговоре. Полный отчёт по тому же сертификату приезжает одной строкой в 95 707 знаков, 450 строк:

flang --mcp-mode < zapros.jsonl | tail -1 | python3 -c \
 'import json,sys; t=json.load(sys.stdin)["result"]["content"][0]["text"]; print(len(t), t.count(chr(10))+1)'

Отсюда правило: flang_check — на программу, которую пишете сейчас; flang_prove с именем обещания — на всё, что крупнее. Второй отвечает одним абзацем вместо ста страниц.

Чего служба не делает

Она не мешает помощнику написать неверное. Она отнимает у него возможность назвать неверное правильным: «эта функция корректна» — предложение, а доказано в ответе — результат прогона.

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

Дальше