flang 0.7.27 — Доказательства по-взрослому: алгебра, завершение рекурсии, формулы в LaTeX; HTTPS без curl

Доказательства по-взрослому: алгебра, завершение рекурсии, формулы в LaTeX; HTTPS без curl

Что появилось

• Ядро доказывает алгебраические тождества над целыми. check --proof раскрывает обе стороны равенства в многочлен и сравнивает их. Это аналог тактики ring в Lean. Например, (a + b)·(a + b) = a·a + a·b + b·a + b·b доказывается для всех точных целых a и b. Для число, то есть для double, такие законы ложны, поэтому там будет отказ с объяснением.
• Доказательства перепроверяют две независимые программы, на C и на Lean 4. Ядро записывает доказательство в файл, а обе программы перепроверяют его каждая по-своему. Если ядро ошибётся или запись подделают, это поймают. Что перепроверить не удалось, check --proof называет прямо. Обе проверки идут в CI на каждом пуше.
• Компилятор доказывает, что рекурсия завершается. Пишете у функции убывает н, и check либо доказывает, что н уменьшается при каждом вызове, либо отказывает с кодом FLANG_NOT_TOTAL. Так, н минус 1 на неотрицательных доказывается, а шаг вида 3·н + 1 (Коллатц) отвергается сразу, ещё до запуска.
• Доказанное свойство функции используется в других доказательствах. Если доказано, что f(x) равно какому-то выражению, ядро подставит это выражение везде, где встретится вызов f. Это аналог simp. Цепочка из 18 вложенных вызовов доказывается.
• Формулы можно писать как в учебнике. formula:read '∀ a ∈ ℤ, ∀ b ∈ ℤ, a + b = b + a' или та же формула в LaTeX превращается в утверждение flang, и его сразу проверяет ядро. Работает и обратно: formula:print файл.flang печатает утверждения файла как формулы и как LaTeX. ℕ означает точные целые, ℤ — 53-битные целые (переводчик об этом предупреждает), ℚ≥0 — точные дроби. ℝ и ℂ не поддерживаются: double не подчиняется законам поля.
• Длинное выражение можно переносить на новую строку внутри круглых скобок. Отступ продолжения не важен, ошибка указывает настоящие строку и столбец.
• Законы моноида, функтора, монады и изоморфизма проверяются при компиляции. Компилятор подставляет набор значений и ищет контрпример. Нарушенный закон даёт код 1, непроверенный — код 2. Это проверка на примерах, а не доказательство, и компилятор пишет это прямо. В flang/ct добавлено восемь примеров по теории категорий: произведение, копроизведение, пулбэк, сопряжение, лемма Йонеды на предпорядке, моноидальная категория, Maybe как моноид, стрелки Клейсли.
• HTTPS работает без curl. Клиент TLS 1.3 написан на flang и встроен в двоичный файл. Корневые сертификаты берутся из системы или из --trust-roots файл.pem. Добавлены отправка и приём UDP.
• Скрипты (.fscript) компилируются в C, Go, Rust и Python. flang_cli --plan <имя> запускает план в выбранном языке. Работают файлы, каталоги, переменные среды и аргументы. Остальные операции пока отвечают ошибкой FLANG_IO_NOT_WIRED.
• Сообщения компилятора по-английски. Задайте FLANG_LANG=en или language = en в .flangrc. Переводы лежат в обычной таблице flang/messages/catalog.tsv.
• Сгенерированный код проверяет типы на входе. Во всех десяти целевых языках программа отвергает вход, который не подходит под объявленный тип. Например, отрицательное число там, где объявлено неотрицательное.

Что изменилось

• Ошибка связывания модулей называет файл: сообщение начинается с в файле <путь>:.

Что сломалось

• HTTPS больше не вызывает curl. Если двоичный собран без встроенного клиента TLS (в том числе flang emit --repl), запрос по https отвечает FLANG_IO_NO_TLS. Отключить проверку сертификатов нельзя.
• Функция с убывает, у которой мера не уменьшается, теперь не проходит check (FLANG_NOT_TOTAL, код 1). Раньше она падала только при запуске.
• Конфликт имён при импорте теперь ошибка. Это случай, когда импортированная функция зовёт скрытого помощника своего модуля, а в другом файле есть одноимённый. Ошибка — FLANG_DUPLICATE_NAME. Чтобы исправить, добавьте помощника в список только или переименуйте его.
• Неверный закон моноида, монады или функтора — теперь код 1 у check. Раньше такие законы не проверялись.
• Неверный по типу вход сгенерированной программы — теперь FLANG_TYPE во всех целевых языках.

Описание языка

Разделы DESCRIPTION.md, изменённые с v0.7.26:

• Синтаксис
• Целевые языки
• Файл настроек
• Ограничения

---

Grown-up proofs: algebra, terminating recursion, LaTeX formulas; HTTPS without curl

What appeared

• The kernel proves algebraic identities over integers. check --proof expands both sides of an equality into a polynomial and compares them, like Lean's ring. For example, (a + b)·(a + b) = a·a + a·b + b·a + b·b is proved for all exact integers a and b. Over число (double) these laws are false, so you get a refusal that says why.
• Proofs are re-checked by two independent programs, one in C and one in Lean 4. The kernel writes the proof to a file, and each checker replays it on its own. A kernel bug or a forged record gets caught; whatever could not be replayed, check --proof names. Both checks run in CI on every push.
• The compiler proves that recursion terminates. Write убывает н (decreases n) on a function, and check either proves that н shrinks on every call or refuses with FLANG_NOT_TOTAL. н минус 1 over non-negative numbers is proved; a 3·н + 1 step (Collatz) is rejected at compile time, before anything runs.
• A proved property of a function is used in other proofs. Once f(x) is proved equal to some expression, the kernel substitutes that expression wherever f is called, like simp. A chain of 18 nested calls is proved.
• Write formulas as in a textbook. formula:read '∀ a ∈ ℤ, ∀ b ∈ ℤ, a + b = b + a', or the same formula in LaTeX, becomes a flang statement that the kernel checks right away. It also works the other way: formula:print file.flang prints a file's statements as formulas and as LaTeX. ℕ means exact integers, ℤ means 53-bit integers (the translator warns you), ℚ≥0 means exact fractions. ℝ and ℂ are not supported, because double does not obey the field laws.
• A long expression can wrap onto the next line inside parentheses. The continuation indent does not matter, and errors point at the real line and column.
• Monoid, functor, monad and isomorphism laws are checked at compile time. The compiler tries a set of values and looks for a counterexample. A broken law is exit code 1, an unchecked one is code 2. This is testing, not proof, and the compiler says so. flang/ct gains eight category theory examples: product, coproduct, pullback, an adjunction, the Yoneda lemma on a preorder, a monoidal category, Maybe as a monoid, Kleisli arrows.
• HTTPS works without curl. A TLS 1.3 client written in flang is built into the binary. Root certificates come from the system or from --trust-roots file.pem. UDP send and receive were added.
• Scripts (.fscript) compile to C, Go, Rust and Python. flang_cli --plan <name> runs a plan in the chosen language. Files, directories, environment variables and arguments work; other operations answer FLANG_IO_NOT_WIRED for now.
• Compiler messages in English. Set FLANG_LANG=en or language = en in .flangrc. Translations live in a plain table, flang/messages/catalog.tsv.
• Generated code checks types at its input. In all ten target languages the program rejects input that does not match the declared type, such as a negative number where неотрицательное (non-negative) is declared.

What changed

• A module linking error names the file: the message starts with в файле <path>:.

What broke

• HTTPS no longer calls curl. A binary built without the embedded TLS client (including flang emit --repl) answers an https request with FLANG_IO_NO_TLS. Certificate checking cannot be turned off.
• A function with убывает whose measure does not shrink now fails check (FLANG_NOT_TOTAL, code 1). Before, it only failed at run time.
• An import name clash is now an error. This is the case where an imported function calls a hidden helper of its own module and another file has a helper of the same name. The error is FLANG_DUPLICATE_NAME. Fix it by listing the helper in только or renaming it.
• A wrong monoid, monad or functor law is now exit code 1 from check. These laws were not checked before.
• Badly typed input to a generated program is now FLANG_TYPE in every target language.

---

Страница выпусков: по-русски · in English.

Архив flang-0.7.27-c.tar.gz — исходники C99 и Makefile: make && sudo make install, Node не нужен. Или brew install digitable-lol/tap/flang.