flang — язык, в котором спецификация исполняется

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

Здесь выбран другой путь. Спецификация и есть программа. Правила пишутся один раз, исполняются, проверяются собственными примерами — а потом печатаются в C, Go, Rust, Python, Java, C# или Elixir, где напечатанный код обязан выдавать те же значения и те же коды ошибок, что интерпретатор, вход за входом.

тотальная функция «Произведение»
  принимает элементы: список числа
  возвращает число
  пример «Произведение четырёх»
    дано элементы равно [1, 2, 3, 4]
    ожидается 24
  пример «Произведение пустого — единица»
    дано элементы равно пустой список
    ожидается 1
  свёртка элементы начиная с 1 как акк и эл → акк умножить на эл

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

Три вещи, которых нет у обычных языков

Завершаемость доказана при компиляции. В C, Python и JavaScript функция может зациклиться, и вы узнаете об этом в бою. Здесь тотальная — обещание, за которое отвечает компилятор: 4893 функции из 6429 его несут.

Обещание о результате проверяется на всех входах, а не на примерах. Тесты покрывают те входы, до которых вы додумались. Постусловие, принятое ядром доказательств, — все.

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

Чем мы отличаемся от Coq, Agda и Lean

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

flang пробует закрыть эту пропасть: один язык, на котором и доказывают, и пишут обычный код, и который при этом читается.

Ядро доказательств не принимает на веру ничего. Аксиом ноль, и список пуст проверяемо — отдельным тестом, тихо добавить нельзя. Решающих правил три, и каждое можно прочесть целиком.

Где мы на самом деле

Цифры измеряются прогоном, а не оцениваются, и обновляются вместе с деревом.

И честно про то, чего нет:

• обычных функций библиотеки доказывается 7 из 20 — замер брал каждую девятую из всех 185, чтобы не выбирать удобные;
• язык медленнее Python в 1,4 раза, и это не цена доказуемости: она измерена и равна 2,5 % — платит 71 функция из 2799. Остальное — обычная неоптимизированность, и она чинится;
• компилятор написан на flang не целиком: цепочка доказательства — да, а семь генераторов кода, процессы, оболочка — пока нет.

С чего начать

• Первая программа — поставить и запустить за пять минут.
• Зачем доказательства и как они устроены — главное отличие языка.
• Спецификация языка — что в нём есть.
• Что доказано, а что проверено — граница проведена явно, и это важно.
• База знаний — почему решения приняты так, что измерено и что оказалось ложным.