Цеттелькастен flang

База знаний проекта. Здесь лежит не то, что сделано — это говорит история коммитов, — а почему решили так: что померили, что оказалось ложным, какие пути отвергли и по какому доводу.

Проверка на годность заметки: она отвечает на вопрос, который встанет снова.

Как пользоваться

Заголовок каждой заметки — утверждение, а не тема. Читать можно с любой: ссылки [[слаг]] ведут к соседям, и через два-три перехода собирается вся линия рассуждения.

Если ищете конкретное — смотрите группы ниже. Если хотите понять проект с нуля — начните с цели и идите по ссылкам.

Цель и рамки

• Цель flang — доказуемость, доступная обычному программисту
• Из восьми целей печати важна только C, остальное отложено
• Революция наступит ровно тогда, когда доказательство станет дешевле тестов
• Разрыв между «доказано» и «правильно» — это спецификация
• Развилки, которые владелец выбрал сам
• Отчёты пишутся простым инженерным языком, без проектного жаргона

Числа

• Биты плавающей точки точны; неточен перевод десятичной записи в двоичную
• Вопрос не «точно или приблизительно», а «точно в какой системе счисления»
• Точные десятичные стоят ноль, а не в сто раз дороже
• Языку нужны три типа чисел с разными гарантиями
• У double ломается ассоциативность, а равенство даже не рефлексивно
• Бесконечность становится законной, если убрать вычитание
• Числа описываются категорией, но категория не вычисляет

Доказательства

• Узкое место прувера — сила правил, а не ненаписанные доказательства
• Невысказываемое утверждение дороже недоказуемого
• Сила Coq не в ядре, а в библиотеке доказанных лемм
• Поиск доказательства не должен ничему верить
• Ноль аксиом — проверяемое свойство, а не лозунг
• Цена доказательства измерена: 0 из 20, и тесты нашли четыре ошибки против нуля
• Принципа индукции нет ни у одного встроенного типа
• Узкое место переехало: принцип индукции появился, а цепляться ему не за что
• Тавтология закрывается даром, поэтому число «доказано без теоремы» само по себе ничего не значит

• Замкнутую цель надо считать, а не выводить
• Узкое место переехало третий раз: мешает форма утверждения, а не форма тела
• Свёртка в flang левая, и индукцию по списку к ней прицепить нельзя

Теория категорий

• Теоркат переносит правду между вещами; логика устанавливает её про одну вещь
• Естественное преобразование ловит ошибку, которую не видит больше ничто
• Связь двух модулей становится проверяемой ровно тогда, когда назван перевод данных

Память

• Память «на категорию» — это регионы, техника с именем
• Область памяти не отдаёт ничего до конца вызова: 1655 МиБ на сортировку 4000 чисел
• Для критичных систем стандарты запрещают динамическую память вообще
• Чистота означает «без изменения на месте», а не «без выделения памяти»
• Игры и обработка видео — не наш случай, и причин ровно три

Скорость и цена доказуемости

• Цена доказуемости — 2,5 % функций, а всё остальное медленно по другим причинам
• Мы медленнее Python в 1,4 раза, и компиляция сегодня не окупается никогда
• Две правки дают 1,8 раза, и одна из них — две строки
• Вывод типов отдаёт доказанное отметкой на дереве, а не таблицей наружу
• Снятая проверка типа даёт не отказ, а неверный ответ
• Межмодульная оптимизация ускорила не только работу, но и сборку большого файла

Процессы и конкурентность

• BEAM не обходит операционную систему, и C зависит от неё ровно так же
• Динамическое порождение процессов есть в модели и в C, а нет — у двух целей печати
• Планировщик тянет миллион работающих процессов, а стена осталась одна из трёх — очередь готовых

Самораскрутка и метод проверки

• Дважды за один замер врал прибор, а не предмет — и оба раза это выглядело как находка

• Самораскрутка меряется четырьмя кусками JavaScript, три закрыты
• Побайтовая сверка с эталоном — главный метод проверки
• Побайтовая сверка данных не видит зависимости от тождества объектов
• Вторую независимую реализацию возместить нечем — её можно только сохранить в проверках
• Снятая правка обязана красить тест
• Проверка, переставшая сравнивать, продолжает зеленеть
• Бывают конфликты слияния, которых git не показывает
• Два ядра, выросшие порознь от одной точки, текстом не сливаются
• Долг, закрытый на неслитой ветке, остаётся открытым долгом
• Близнец отстаёт от эталона, который уехал, — отставание надо мерить
• Измеренный ноль ценнее ненайденного правила
• Замер скорости проверяет себя контрольной суммой
• Переименование файла не краснеет, а тихо выключает проверку чисел в прозе
• Вторую сторону сверки можно заморозить, но проверка меняет род
• Перечень, записанный в проверке руками, переживает дерево
• Команда может ответить «проверено», не проверив ничего
• Число прозы без названного измерителя не перепроверяется, а заменяется другим числом
• Относительная ссылка ломается ровно при копировании каталога

Устройство репозитория

• Старый проект FTS нельзя вынести дёшево: от него зависят все восемь генераторов кода flang

Найденные ошибки

• Ядро печатало «доказано индукцией» об утверждении, которое рантайм отвергал
• Поле записи отмывало значение из-за симметричного сравнения типов
• NaN достижим изнутри языка и делает «очевидные» правила ложными
• Ядро принимает ложь дважды за сутки — это класс дефектов
• Минус ноль всплыл четыре раза — это класс, а не отдельные ошибки
• В WebAssembly нет сторожевой страницы, поэтому заниженная константа стека портит память молча

Отвергнутые пути

• Автоматический вывод регионов — мимо цели, а не дорого
• Z3 можно взять оракулом, нельзя судьёй
• [Чтение условий если закрывает ноль целей](usloviya-esli-dali-nol.md)

Модульность и пакеты

• Адресация по содержимому: версий нет, есть хеши
• Unison установлен и измерен: ромб он решает не так, как обещает лозунг
• Гипотеза про адресацию по содержимому не работает у нас — и не из-за хешей
• В хеш входит контракт, но не доказательство — у теоремы свой адрес
• Хеш содержимого — идентичность внутри, имена и версии — интерфейс снаружи

Внешнее и объёмы

• Что в популярных рассказах о доказуемых языках верно, а что ложно
• Свой генератор машинного кода — примерно месяц, и на доказуемость не влияет
• WebAssembly получается через C даром: девятая цель печати не нужна

Передача работы

• [Состояние проекта передаётся файлом docs/PEREDACHA.md, а не пересказом](peredacha-sostoyaniya.md)

Начинаете работу с чистого листа или с другой учётной записи — читайте передачу состояния первой. Там пути, ветки, что сделано, чего не хватает, что делать дальше по отдаче и чего делать нельзя. Здесь — почему решили так; там — где мы сейчас. Что это за файл и почему он один, сказано в заметке Состояние проекта передаётся файлом, а не пересказом.

Лежит он в двух местах, и путь к нему зависит от того, откуда вы читаете:

Ссылки здесь нарочно нет, и это не небрежность. Относительный путь верен ровно в одном из двух мест: ../PEREDACHA.md из репозитория попадает в docs/PEREDACHA.md, а из копии — в /srv/PEREDACHA.md, которого не существует. Ломалась при этом та самая ссылка, ради которой абзац написан: её читают, зайдя с другой учётной записи, то есть как раз через копию. Оба пути названы текстом — тогда самодостаточны оба места. Ссылки на соседние заметки этой беды не имеют: они лежат рядом и в репозитории, и в копии.

Как добавлять

Одна заметка — одна мысль. Формат:

# Заголовок-утверждение, а не тема

Суть в первом абзаце.

**Чем подтверждено.** Число, прогон, ветка и коммит — чтобы можно было проверить.

**Чем ограничено.** Где это перестаёт быть верным.

Связано: [[слаг-соседа]], [[другой-слаг]]

Правила:

1. Заголовок — утверждение. «Ассоциативность у double не держится», а не «Про ассоциативность». Если заголовок не утверждение, заметка ещё не додумана.
2. Числа с происхождением. Измеренное отделять от оценённого прямо в тексте.
3. Простым языком — пояснение.
4. Ссылка на несуществующую заметку — не ошибка. Она помечает то, что стоит написать.
5. Отрицательный результат — полноценная заметка. Отвергнутый путь с доводом экономит больше, чем ещё одно описание успеха.

Добавили заметку — впишите строку в этот индекс.