Замер цены доказательства: 20 обычных функций, обе работы, измеренные числа

Вопрос, ради которого замер сделан: дешевле ли доказать функцию, чем написать на неё тесты? Число это в проекте не мерили ни разу. Здесь оно померено впервые — и получилось не то, чего ждали.

Основание — чтобы число было с чем сравнивать потом

Ядро сейчас двигают несколько веток; всё ниже посчитано на origin/main и ни на чём другом. Повторить замер на другой ветке — значит получить другое число, и сравнивать их можно только назвав оба основания.

Ответы на четыре вопроса — сразу, без предисловий

1. Отношение цены: доказательство против тестов

Отношение цены посчитать честно нельзя, и это главный результат первой строки отчёта. Цена — это плата за результат; здесь одна из двух работ результата не дала вовсе. Доказательство обошлось в 196 строк и 9,7 минуты и не закрыло ни одного утверждения из двадцати. Правильная формулировка не «в N раз дороже», а «тесты стоят 19,5 строки на функцию и работают; доказательство стоит 9,8 строки на функцию и не работает ни на одной».

Строки доказательства при этом честно посчитаны как написанные, а не как принятые: постусловие, теорема и функции-помощники, написанные только ради того, чтобы утверждение вообще можно было выговорить.

2. Доля бесплатных: сколько ядро закрыло само

0 из 20. Ни одного случая, где утверждение о функции закрылось бы без написанной теоремы. И ни одного, где закрылось бы с написанной.

Для сравнения: во всём дереве репозитория сегодня 9 высказанных утверждений, из них 115 доказаны ядром (npm run proof:ledger) — на 2799 функций. Замер не опроверг эти шесть, он показал, насколько узко место, из которого они взяты. Чтобы ядро закрыло утверждение, должны сойтись три условия сразу:

1. параметр — объявленная сумма (тип … вариант …), а не встроенный тип;
2. тело функции — **разбор по этому самому параметру**;
3. у каждого конструктора суммы поля либо отсутствуют вовсе (тогда случай закрывается вычислением примера), либо есть поле типа самой суммы (тогда случай закрывается предположением индукции).

Первые два условия в выборке из двадцати сошлись у трёх функций (01, 02, 16). Третье не выполнено ни у одной: у «Связи», «Звена», «Успеха» и «Ошибки» поля есть, но все они чужого типа — строки и параметры типа. Такая посылка не закрывается ничем: предположения индукции у неё нет («предполагать не о чем»), примером её тоже не закрыть («связывает имена, значений бесконечно много»). Оба отказа советуют ровно то, что запрещает другой.

3. Что мешает чаще всего — и сколько случаев уперлось в невыразимость

Главная причина «ядро не берёт» — одна и та же на 13 функциях из 15, и она называется одной строкой отказа:

FLANG_PROOF_INDUCTION_TYPE: индукция теоремы «…» идёт по «элементы», а это не
объявленная сумма. Принцип индукции читается с объявления суммы — у типа без
вариантов его брать негде

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

Невыразимость (5 из 20) распадается на четыре разные дыры, и все четыре — в языке, а не в ядре:

Отдельно и важнее: полное описание того, что функция делает, в язык влезло у четырёх из двадцати. Полностью смысл выразили 4 утверждения (05, 12, 13, 17); в 12 случаях пришлось записать что-то более слабое («длина стала на один больше», «результат не меньше нуля») — и именно это слабое ядро и не взяло; в 4 не вышло ничего (01, 02, 15, 16).

Слова требует в языке действительно нет — и это заметно на «Двоичном поиске», чей договор условен («требует, чтобы список был отсортирован», прямым текстом в комментарии библиотеки). Но замер показал обход, о котором стоит знать: условие записывается импликацией в постусловии — «Следует» от (условие) и (утверждение). Цена обхода: 11 строк на предикат «Отсортирован» и потеря смысла проверки в рантайме — импликация с ложной посылкой истинна, то есть плохой вход такое постусловие пропускает молча, а требует его бы отвергло.

4. Что удешевило бы сильнее всего

По убыванию отдачи, с оценкой работы в строках и с числом функций из двадцати, которые это открывает:

Почему первая строка стоит первой и почему в ней три работы, а не одна. Принцип индукции для списка сам по себе открывает только 2 функции из двадцати (07,

1. — те, чьё тело есть разбор по списковому параметру. Ещё 5 (03, 06, 11,

17, 18) написаны свёрткой, и им нужна развёртка свёртки на конструкторе: это законно и не новое понятие — то же универсальное свойство начальной алгебры, из которого читается сама индукция. Отсюда «до 7 из 20».

Оставшиеся 13 первой работой не открываются, и стоит сказать, чем именно: у 04, 08, 10, 14, 19, 20 тело — вызов другой функции, а по свойству «…» на постусловие ДРУГОЙ функции ядро сегодня отвергает (сличение по вызову не сделано); 05, 12, 13 — не про списки вовсе; 01, 02, 15, 16 не выразимы.

И третья часть работы, без которой первые две ничего не закрывают: целям вида «длина результата на один больше» нужна таблица перепи́сок для встроенных форм — длина (добавить х к с) → длина с плюс 1, длина пустой список → 0, (добавить х к с) содержит х → да. Каждая такая переписка — теорема о встроенной форме, ровно как два нынешних правила reduce.mjs суть теоремы о IEEE-754, и проверяться она обязана враждебной выборкой так же. Кстати, последняя из трёх закрывает функцию 03 в одиночку, вообще без индукции.

Отдельно: ядро принимает ложь. Найдено этим замером

Это не про цену, но молчать об этом нельзя, потому что оно обесценивает слово «доказано» целиком.

**Шаг по примеру, стоящий НЕ внутри индукции, не проверяет замкнутость цели вовсе.** Проверка есть — и в flang/proof/SPEC.md она названа «главной проверкой состоятельности этого правила», — но живёт она в ветке случайВарианта !== null функции поПримеру (flang/src/proofterm.mjs). Прямой шаг в эту ветку не заходит: посылка у него undefined, проверка пропускается, дальше идёт прогон ОДНОГО примера и вердикт СИЛА.proved.

Улика целиком (файл собирается за минуту, воспроизводится на origin/main):

модуль «Подделка»

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

теорема «результат не больше нуля»
  дано х: число
  утверждаем результат не больше 0
  по примеру «Пять»
  следовательно доказано

Что говорит ведомость:

постусловие «результат не больше нуля» функции «Противоположное» —
доказано: терм принят ядром, 1 шаг — утверждение обо ВСЕХ входах

Что говорит тот же интерпретатор на том же файле:

$ flang run … --function 'Противоположное' --args '{"х": -5}'
{"error":"нарушено свойство «результат не больше нуля» функции «Противоположное»"}

То есть ядро печатает «доказано обо ВСЕХ входах» про утверждение, для которого контрпример находится в том же файле и той же командой. Утверждение ложно, пример один и он проходит — этого хватило.

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

Кого это касается прямо сейчас. Шесть доказанных утверждений корпуса проверены индукцией и в эту ветку не попадают — их вердикт от находки не меняется. Но любое новое утверждение, закрытое прямым по примеру, сегодня ничем не отличается от «мы посмотрели один пример».

Что нашла работа: четыре настоящие ошибки, и все четыре — тестами

Все четыре воспроизводятся на нетронутых файлах библиотеки, не на копиях замера.

**1. «Чётное» от любого отрицательного числа отвечает «нет».**

$ flang run flang/stdlib/numbers.flang --function 'Чётное' --args '{"число": -4}'
{"result":false}

Причина: -4 остаток от 2 в IEEE-754 равно -0, а равенство скаляров считает Object.is (flang/src/builtins.mjs, valuesEqual), для которого -0 и 0 — разные значения. Примеры автора стоят на 4 и 5, поэтому беда прожила в библиотеке незамеченной. Тем же корнем сломаны «Делится на» (-4 на 2 → нет) и вторая копия «Чётное» в higher-order.flang.

**2. «Уникальные» оставляет в ответе два нуля.**

$ flang run flang/stdlib/lists.flang --function 'Уникальные' --args '{"элементы": [0, -0, 1]}'
{"result":[0,0,1]}

Тот же Object.is: -0 не считается уже встреченным.

**3. «Строчная буква» от пустой строки — отказ, а функция объявлена тотальной.**

$ flang run flang/stdlib/strings.flang --function 'Строчная буква' --args '{"буква": ""}'
{"error":"«разделить»: разделитель не может быть пустым","code":"FLANG_BUILTIN_ARGS"}

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

**4. «Строчная буква» от "AB" отдаёт "a"** — молча портит вход, вместо того чтобы вернуть его как есть (как она поступает с "7" и с "Б").

Чем нашли. Все четыре — обычными примерами: отрицательное число, -0, пустая строка, две буквы. Написание постусловия помогло в двух случаях из четырёх (13 и

1. — но только потому, что рядом уже стоял пример с нужным входом: постусловие

считается на сетке примеров автора, и без примера с -4 оно молчало бы так же, как молчало в библиотеке. Само по себе постусловие не ищет входов.

Пятая находка — дыра в состоятельности ядра — найдена стороной доказательства. Это единственное, что доказательства нашли, и это находка про инструмент, а не про функцию.

Как отбирали двадцать — воспроизводимо и не в нашу пользу

1. Корпус — все функции flang/stdlib/*.flang (12 модулей): списки, строки, числа, записи, словари, деревья. Это ровно тот материал, о котором задан вопрос, и он не выбран под удобство — библиотека написана задолго до замера.
2. Порядок — «файл по алфавиту, внутри файла по порядку объявления». Никакой сортировки по вкусу.
3. Отбор годных — «нет ни постусловия, ни теоремы». Годными оказались все 185 функций из 185: в flang/stdlib нет ни одного утверждения о поведении.
4. Выборка — каждая девятая (шаг = ⌊185 / 20⌋ = 9), индексы 0, 9, 18, …,
   1. Двадцать штук.

Скрипт отбора: flang/src/parser.mjs + перебор, воспроизводится за минуту; список получившихся двадцати — в таблице ниже, у каждой указан файл и строка оригинала.

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

Вторая оговорка, тоже против нас. Ни одно утверждение нельзя написать рядом с функцией: flang/stdlib входит в корпус побайтовой неподвижной точки самоприменения, а у восьми слов доказательства нет продукции в flang/self/parser.flang. Поэтому все двадцать функций скопированы в отдельные файлы. Копирование в измеренные строки не включено — иначе доказательство выглядело бы дороже, чем оно есть.

Оговорка снята 15 августа 2026, и это меняет условия, а не числа замера. Продукции всех восьми слов написаны, запрет на слова доказательства в flang/stdlib переделан из запрета в счёт, и постусловия там уже стоят — numbers.flang, higher-order.flang, logic.flang, strings.flang. Скопировать пришлось бы не двадцать функций, а те из них, которым нужна ТЕОРЕМА: её берёт сборка программы, а не чтение файла. Числа выше от этого не сдвинулись — копирование в них и не входило, — но повторять замер надо уже в новых условиях.

Таблица: все двадцать, обе работы, оба исхода

¹ Формально ядро приняло здесь терм и напечатало «доказано» — но приняло по неисправному правилу (см. раздел про состоятельность), поэтому в счёт доказанного случай не зачтён. Зачесть его значило бы подогнать замер.

Единственная переписка на тестовой стороне — функция 14: ожидание было моё, а поведение библиотеки правильное («равное уходит вправо и не теряется» — прямо сказано в её примерах). Это цена тестов, а не находка: тест бывает неправ, и переписывать приходится его.

Время по функциям (секунды, тесты / доказательство): 18/82, 14/22, 32/46, 20/45, 12/101, 28/19, 26/10, 19/31, 24/21, 35/15, 47/6, 13/17, 13/43, 27/28, 15/21, 26/23, 27/15, 15/10, 42/15, 16/9.

Про время — прямо. Это машинное время работы агента с секундомером, а не время человека; в нём заметна доля ожидания инструментов. Пользоваться им можно только внутри самого замера, для сравнения двух сторон между собой. И там видна кривая обучения, которая работает В ПОЛЬЗУ доказательств: первая попытка стоила 82 и 101 секунду, последние — 9 и 10, потому что ответ «ядро не возьмёт» стал виден без единого запуска. Если бы ядро брало, эта кривая была бы аргументом «дальше дешевле»; здесь она означает только, что быстро научаешься не пытаться.

Как это выглядит на глаз: по примерам на каждый исход

Исход «ядро не берёт» — правда высказана, правил не хватает

**Пример А. «Есть в множестве» (docs/zamer/17-est-v-mnozhestve.flang).** Утверждение здесь ПОЛНОЕ — оно исчерпывает смысл функции, а не ослабляет его:

тотальная функция «Есть в множестве»
  принимает множество: список строки, искомое: строка
  возвращает признак
  для всех множество обеспечивает «это и есть вхождение» результат равен (множество содержит искомое)
  // ── ТЕСТЫ: 7 примеров, 28 строк ──
  пример «Элемент есть»
    дано множество равно ["а", "б", "в"]
    дано искомое равно "б"
    ожидается да
  пример «Элемента нет»
    дано множество равно ["а", "б"]
    дано искомое равно "я"
    ожидается нет
  пример «В пустом множестве нет ничего»
    дано множество равно []
    дано искомое равно "а"
    ожидается нет
  пример «Первый элемент находится»
    дано множество равно ["а", "б"]
    дано искомое равно "а"
    ожидается да
  пример «Последний элемент находится»
    дано множество равно ["а", "б"]
    дано искомое равно "б"
    ожидается да
  пример «Пустая строка — обычный элемент»
    дано множество равно ["", "а"]
    дано искомое равно ""
    ожидается да
  пример «Регистр различается»
    дано множество равно ["А"]
    дано искомое равно "а"
    ожидается нет
  // ── КОНЕЦ ТЕСТОВ ──
  свёртка множество начиная с нет как найдено и эл → если эл равно искомое то да иначе найдено

теорема «это и есть вхождение»
  дано множество: список строки
  дано искомое: строка
  утверждаем результат равен (множество содержит искомое)
  индукция по множество
    случай пусто
      то по примеру «В пустом множестве нет ничего»
    случай голова и хвост
      то по предположению
  следовательно доказано

Постусловие типизируется, считается на сетке из семи примеров и не нарушается. Теорема — 9 строк, ровно та же форма, что у доказанной corpus-numtree.flang. Отказ:

FLANG_PROOF_INDUCTION_TYPE: индукция идёт по «множество», а это не объявленная
сумма. Принцип индукции читается с объявления суммы — у типа без вариантов его
брать негде

Разница с доказанной функцией корпуса ровно одна: там параметр — «Дерево чисел», объявленное тип … вариант …, здесь — встроенный список строки.

**Пример Б. «Следует» (docs/zamer/12-sleduet.flang).** Тип обоих параметров — признак, значений у него ДВА, всё утверждение проверяется перебором четырёх строк таблицы:

  для всех посылка обеспечивает «это классическая импликация» результат равен ((не посылка) или следствие)
  …
теорема «это классическая импликация»
  дано посылка: признак
  дано следствие: признак
  утверждаем результат равен ((не посылка) или следствие)
  индукция по посылка
    случай да
      то по примеру «Истина влечёт истину»
    случай нет
      то по примеру «Ложь влечёт истину»
  следовательно доказано

Отказ тот же: признак — не объявленная сумма. При этом ровно такое же доказательство перебором ПРОХОДИТ на «Светофоре» из flang/proof/examples/ — потому что «Светофор» объявлен в программе, а признак встроен. Это самый дешёвый из всех возможных случаев, и он не берётся.

**Пример В. «Вписать» (docs/zamer/03-vpisat.flang).** Здесь видно ещё и то, во что обходится теорема о функции с двумя параметрами:

  обеспечивает «вписанное на месте» результат содержит новое
  …
теорема «вписанное на месте»
  дано звенья: список «Звено»
  дано новое: «Звено»          ← без этой строки: «имя «новое» не связано»
  утверждаем результат содержит новое
  индукция по звенья
    случай пусто
      то по примеру «В пустой список»
    случай голова и хвост
      то по предположению
  следовательно доказано

Первая попытка упала не на ядре, а на области видимости: в теореме видны только имена, введённые дано, поэтому каждый параметр функции надо перечислить заново. Вторая попытка дошла до ядра и получила тот же отказ про список.

Исход «на языке не выразить» — правду нечем записать

**Пример А. «Ключ связи» (docs/zamer/01-klyuch-svyazi.flang).** Функция достаёт поле из записи-суммы. Правда о ней ровно одна: «результат равен полю ключ».

тип «Связь»
  вариант «Связь» содержит ключ: строка, значение: строка

тотальная функция «Ключ связи»
  принимает связь: «Связь»
  возвращает строка
  // ── ТЕСТЫ: 4 примера, 12 строк, зелёные с первого запуска ──
  пример «Обычный ключ»
    дано связь равно вариант «Связь» с ключ равным "имя" и значение равным "Марат"
    ожидается "имя"
  пример «Пустой ключ остаётся пустым»
    дано связь равно вариант «Связь» с ключ равным "" и значение равным "Марат"
    ожидается ""
  пример «Значение на ключ не влияет»
    дано связь равно вариант «Связь» с ключ равным "имя" и значение равным ""
    ожидается "имя"
  пример «Пробелы и юникод в ключе не трогаются»
    дано связь равно вариант «Связь» с ключ равным " ключ 自 " и значение равным "х"
    ожидается " ключ 自 "
  // ── КОНЕЦ ТЕСТОВ ──
  разбор связь
    случай вариант «Связь» с ключ как имя и значение как содержимое
      то имя

Попытка 1 — результат равен связь.ключ:

FLANG_TYPE: доступ к полю «ключ» требует записи, а не «Связь»

Попытка 2 — достать поле разбором прямо в постусловии:

FLANG_PARSE: у 'разбор' нет ни одного 'случай'

разбор требует отступов, а постусловие — однострочное (endLine() сразу после выражения в parseEnsures). Двух способов достать поле суммы нет, потому что нет и одного.

Попытки 3–5 — записать хоть что-нибудь выразимое («длина ключа неотрицательна») и доказать. Тут отказы начинают указывать друг на друга, и это стоит увидеть целиком:

«по предположению» стоит в базе «Связь», где предположения индукции нет:
у этого конструктора нет ни одного поля с типом самой суммы… База закрывается
вычислением — «по примеру»

меняем на «по примеру» —

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

Каждый отказ советует то, что запрещает другой. Это та самая «ближайшая оставшаяся граница», честно названная в flang/proof/SPEC.md, — посылка с непрозрачными полями и без частей.

**Пример Б. «Первый элемент или запасное» (docs/zamer/15-…flang).** Функция полиморфна:

тотальная функция «Первый или запасное заново» от «А»
  принимает элементы: список «А», запасное: «А»
  возвращает «А»
  для всех элементы обеспечивает «на пустом отдаётся запасное» «Следует» от ((длина элементы) равен 0) и (результат равен запасное)

FLANG_TYPE: сравнивать на равенство можно только скаляры, а не «А»

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

**Пример В. «Успешно» (docs/zamer/16-uspeshno.flang).** Смысл функции — «да ровно тогда, когда итог это вариант «Успех»»:

тип «Результат» от «Значение» и «Беда»
  вариант «Успех» содержит значение: «Значение»
  вариант «Ошибка» содержит сообщение: «Беда»

  разбор итог
    случай вариант «Успех» с значение как зн
      то да
    случай вариант «Ошибка» с сообщение как текст
      то нет

Проверки варианта выражением в языке нет вовсе — вариант различает только разбор, а он в постусловие не помещается (та же однострочность). Записать можно было бы только тавтологию результат равен («Успешно» от итог) — утверждение, которое ничего не утверждает. И даже будь оно записано, ядро бы его не взяло по той же причине, что и «Ключ связи»: обе посылки связывают имена полей.

Исход «ядро доказало само» — ни одного, и вот как он выглядит там, где он есть

В выборке из двадцати этого исхода нет. Чтобы было видно, чего именно не хватило, вот единственная форма, в которой он сегодня случается — «Высота» из flang/stdlib/numtree.flang, доказанная в flang/proof/examples/corpus-numtree.flang:

тип «Дерево чисел»
  вариант «Пустое»
  вариант «Развилка» содержит значение: число, меньшие: «Дерево чисел», большие: «Дерево чисел»

тотальная функция «Высота»
  принимает дерево: «Дерево чисел»
  возвращает число
  для всех дерево обеспечивает «высота неотрицательна» результат не меньше 0
  … 3 примера …
  разбор дерево                              ← тело есть РАЗБОР по параметру индукции
    случай вариант «Пустое»
      то 0
    случай вариант «Развилка» с значение как зн и меньшие как м и большие как б
      пусть слева равно «Высота» от м
      пусть справа равно «Высота» от б
      1 плюс (если слева больше справа то слева иначе справа)

теорема «высота неотрицательна»
  дано дерево: «Дерево чисел»
  утверждаем результат не меньше 0
  индукция по дерево
    случай вариант «Пустое»
      то по примеру «У пустого дерева высота ноль»
    случай вариант «Развилка» с значение как зн и меньшие как м и большие как б
      то по предположению
  следовательно доказано

Цена этого успеха: 1 строка постусловия + 9 строк теоремы против 9 строк примеров — то есть на одной удачно устроенной функции доказательство и вправду стоит примерно как тесты. Три условия, которые здесь сошлись все сразу:

1. параметр — объявленная сумма (не список, не строка, не число);
2. тело — **разбор по этому самому параметру**;
3. цель сводится к допущению одним из двух правил reduce.mjs (здесь — «неотрицательность по построению»).

В выборке из двадцати первое условие выполняется у четырёх функций (01, 02, 04, 16); первое и второе вместе — у трёх (01, 02, 16); третье — ни у одной. Все три умирают на одном и том же месте: у их конструкторов есть поля, но ни одно поле не имеет типа самой суммы. Значит предположения индукции нет («предполагать не о чем»), а примером случай не закрыть («связывает имена, значений бесконечно много»). Это и есть та самая посылка с непрозрачными полями без частей, которую в flang/proof/SPEC.md обещано закрыть упрощателем.

Чего этот замер не мерил

• Не мерил цену сопровождения. Тесты ломаются при каждом изменении поведения; утверждение переживает переписывание тела. На двадцати функциях за один день это не проверить, и делать вид, что проверено, нельзя.
• Не мерил случай, на котором слой доказательства работает — функцию над объявленной суммой, у которой конструкторы либо без полей вовсе, либо с полем типа самой суммы (дерево, стопка, перечисление). Функции над объявленными суммами в выборку попали — три штуки (01, 02, 16), — но у всех трёх поля чужого типа, и они умерли на третьем условии. Функции «как дерево» в библиотеке есть (numtree, tree), просто каждая девятая в них не попала. Это не поблажка выборке: вопрос был про обычные функции, а обычные функции пишут про списки и строки, и именно они не берутся.
• Не мерил человеческое время. Секундомер стоял на работе агента.
• Не мерил печать в восемь целей — постусловия печатаются, и цена этого в замер не входила.

Вывод одним абзацем

Сегодня доказательство в flang не дороже тестов — оно невозможно на обычной функции. Двадцать функций из двадцати остались недоказанными, и тринадцать упёрлись в одну дыру: у встроенных типов — списка, строки, числа, признака — нет принципа индукции, а обычный код написан про них. Ещё пять упёрлись в то, что правду о функции нечем выговорить: поле суммы из выражения не достать, вариант не проверить, значения параметрического типа не сравнить. Тесты за то же время нашли четыре настоящие ошибки в библиотеке; доказательства нашли одну — в самом ядре, и эта одна серьёзнее всех четырёх, потому что делает слово «доказано» ненадёжным. Пока не закрыты пункты 1 и 2 из списка удешевления, отношение цены измерять рано: измерять нечего.