Из двух половин доставки язык доказывает только «не больше одного»

Распределённость flang даёт at-most-once: сообщение через границу узла либо приходит ровно один раз, либо не приходит вовсе, и отправитель об этом не узнаёт. Это измерено по коду, а не взято из документа: в flang/conc/distributed.mjs нет ни повторной посылки, ни подтверждения, ни номера сообщения, ни таблицы виденного. Отправка — одна запись в сокет и возврат легло.

Половина «не больше одного» выразима на flang и доказана. Половина «не менее одного» не выразима вовсе, и это не недоделка.

Как записана доказуемая половина. В flang/self/distributed.flang заведён тип «Исход отправки» с четырьмя вариантами (адресат здесь, через границу, связь потеряна, адресата нет) и функция «Кадры отправки», возвращающая список кадров. Утверждение — (длина результат) не больше 1 — доказано индукцией по типу: база 4 случая, обо ВСЕХ входах типа, а не о написанных.

Это не тавтология: три ветки из четырёх дают пустой список, одна — список из одного элемента, и утверждение проверяет именно то, что повторной посылки нет НИ В ОДНОЙ ветке. Сломай любую — и число перестанет быть верным.

Почему вторая половина не выразима. «Письмо дойдёт» — утверждение про сеть, а про сеть язык не говорит ничего: у программы на flang есть аргументы и результат. Узел, который молчит, неотличим от узла, который умер (Fischer, Lynch, Paterson, 1985), и никакой срок этого не меняет — он меняет только то, когда мы перестанем ждать. Чтобы обещать «не менее одного», пришлось бы завести аксиому о надёжности сети, а список аксиом в проекте пуст и обязан таким остаться (zero-axioms).

Цена выбора, названная числом. Обработчик flang чист и возвращает новое состояние значением, поэтому повторная доставка сложилась бы в состояние дважды. Чтобы «не менее одного» было безопасно, каждый обработчик обязан был бы стать идемпотентным — а идемпотентность в языке нечем выразить и нечем проверить, в отличие от тотальности, запаса витков и полноты разбора, которые проверяются. Перекладывать на автора обязанность, которую язык не умеет описать, — ровно то, чего модель избегает везде.

Что доказывается даром рядом. «Если сообщение доставлено, обработчик завершится» — следствие тотальности, и оно посчитано: в корпусе 25 обработчиков, у 22 завершение доказано компилятором. У оставшихся трёх (flang/conc/examples/budget.flang, examples/web/shortener/handler-without-budget.flang, examples/web/shortener/server.flang) тотальности нет, и завершение несёт проверка запаса витков при работе: обработчик кончится, но отказом FLANG_BUDGET_EXHAUSTED, а не результатом. Это разные обещания, и путать их нельзя.

Чем подтверждено. flang/self/distributed.flang (901 строка) и flang/test/self-distributed.test.mjs: 395 значений корпуса, 5 297 491 байт побайтовой сверки со свидетелем, 0 расхождений; ведомость доказательства — flang check --proof. Ветка work/uzly, 18 августа 2026.

Чем ограничено. Доказано про кадры, которые узел ПОРОЖДАЕТ, а не про кадры, которые доходят. Про порядок после разрыва не доказано ничего: часть писем потеряна навсегда, новая связь начинает с чистого листа, дыру в потоке никто не нумерует и не обнаруживает.

Связано: zero-axioms, proven-is-not-correct, unstatable-costs-more-than-unprovable, tautologies-close-for-free, byte-for-byte-comparison