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

Цена доказуемости — 2,5 % функций, а всё остальное медленно по другим причинам

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

Счётчики шагов, глубины и стека — 0,9–8,9 %, целиком внутри разброса прибора. Три независимые проверки; на двух задачах сборка «без пределов» вышла даже медленнее базовой, то есть величина неразличима. Убирать их не надо — экономии не будет, а гарантии исчезнут.

Что платит измеримо:

ценасколько функций
сторож объявленной мерыутраивает функцию (479 мс против 156)66
топливо+33 %5
итого71 из 2799 — 2,5 %

При компиляции доказательства ещё дешевле. Анализ завершаемости плюс ядро — 15,8 мс из 520 нашей части и 0,09 % всего пути от исходника до бинарника. Путь дожимает не мы, а cc: наши 1,2 с против 17 с у сборки.

Как этим пользоваться. Когда кто-то говорит «доказуемость дорого стоит» — вот число. Дорого стоит не доказуемость, а неоптимизированный генератор кода: slower-than-python-by-1-4 и biggest-win-for-least-work.

Ветка work/zamer-skorosti, отчёт docs/benchmark-speed.md, 997 строк, стенды в benchmarks/speed/.

Связано: slower-than-python-by-1-4, condition-for-the-revolution, checksum-inside-the-benchmark, biggest-win-for-least-work