flang 0.7.19 — Кванторы дошли до собранного компилятора

Кванторы дошли до собранного компилятора

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

• Теперь можно сказать «для всех элементов этого списка» — и компилятор это докажет. Раньше квантор связывал только простые имена, а про элементы списка сказать было нечем. Работают и вложенные кванторы: «для каждого элемента и для каждого другого элемента».
• Индукция по вашему собственному объявленному типу. Раньше доказать что-то про свой тип разбором случаев было нельзя — правила знали только встроенные типы.
• Утверждение можно писать не при функции, а само по себе: «утверждение «длина любого списка неотрицательна»». Такие утверждения теперь доходят и до машинного отчёта, и до описи доказанного.
• Шаг доказательства можно назвать словами: шаг теоремы называет правило и посылки, а ядро проверяет, что названное сходится. Раньше шаги были безымянными.
• Компилятор печатает в TypeScript, и справка наконец об этом говорит. Печать работала и раньше, но flang --help о десятой цели молчал: семя отстало от исходников одной строкой.

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

• Правил вывода в ядре стало тринадцать вместо двенадцати — добавилось правило для существования со свидетелем. Теорем в дереве языка 284.
• Установка через Homebrew проверяется целиком. Пять поломок найдено и починено: справка называла девять целей печати при десяти рантаймах в поставке; сообщения об ошибке падали сами на старых оболочках Apple; проверка версии требовала ответа одной строкой, а он нарочно двухстрочный; подсчёт каталогов не ходил по ссылкам, а Homebrew кладёт именно ссылки.
• Английская страница выпусков звала журналы уровнем выше корня сайта — четыре ссылки вели в никуда.
• Правка задачника больше не пересобирает компилятор в облаке: две работы ходили на каждый пуш без разбора.

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

• Доля независимой проверки не выросла: 629 обязательств из 651, те же 96,62 %. Перепечатка семени дала новые умения ядра, а не прирост доли. Мест, где проверка верит компилятору на слово, по-прежнему 12 посылок и 4 шага.
• Верить приходится большему, чем вчера: решающая часть ядра выросла с 4669 строк до 4796. Кванторы живут именно там, вынести их некуда. Наряд снизить это число ниже 4000 остаётся невыполненным.
• О состоянии во времени, побочных эффектах и параллелизме логика по-прежнему не знает ничего. Работа над этими тремя вещами начата, но в этот выпуск не вошла.
• Доказательство относится к flang check и не покрывает собранный код: никто не проверяет, что напечатанный C соответствует исходной программе. Тот же разрыв есть у Coq, Lean и Idris.

---

Quantifiers reached the built compiler

What appeared

• You can now say «for every element of this list», and the compiler will prove it. Previously a quantifier could bind only plain names, and there was no way to speak about list elements. Nested quantifiers work too: «for each element and for each other element».
• Induction over your own declared type. Proving something about your own type by case analysis was impossible before — the rules knew only built-in types.
• A statement can stand on its own rather than beside a function: «statement «the length of any list is non-negative»». Such statements now reach both the machine report and the proved-share ledger.
• A proof step can be named in words: a theorem step names its rule and premises, and the kernel checks that the naming holds. Steps used to be anonymous.
• The compiler emits TypeScript, and the help text finally says so. Emission worked before, but flang --help was silent about the tenth target: the seed lagged the sources by one line.

What changed

• The kernel now has thirteen inference rules instead of twelve — one was added for existence with a witness. There are 284 theorems in the language tree.
• Installation via Homebrew is now checked end to end. Five breakages were found and fixed: the help named nine emit targets while ten runtimes shipped; error messages crashed on their own under older Apple shells; the version check demanded a one-line answer that is deliberately two lines; the directory count did not follow symlinks, and Homebrew installs exactly symlinks.
• The English releases page pointed to the journals one level above the site root — four links led nowhere.
• Editing the task tracker no longer rebuilds the compiler in the cloud: two jobs used to run on every push regardless of content.

What broke

• The independently replayed share did not grow: 629 obligations of 651, the same 96.62 %. Reprinting the seed brought new kernel abilities, not a larger share. Places where the checker takes the compiler's word remain 12 premises and 4 steps.
• More must be trusted than yesterday: the deciding part of the kernel grew from 4669 lines to 4796. Quantifiers live there by construction and cannot be moved out. The work order to bring that number below 4000 remains unmet.
• The logic still knows nothing about state over time, side effects or concurrency. Work on those three has started but did not make this release.
• The proof applies to flang check and does not cover the built binary: nothing verifies that the emitted C matches the source program. Coq, Lean and Idris have the same gap.

---

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

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