Хеш содержимого — идентичность внутри, имена и версии — интерфейс снаружи

Рекомендация по итогам исследования модульности, с ценой.

Схема: содержимое адресуется хешем внутри системы; наружу — обычные имена и версии, как у всех. Не «Unison целиком» и не «пакетный менеджер как у всех», а разделение: хеш решает, что считать одним и тем же; имена решают, как об этом говорить.

Первый шаг — 770 строк. И вот что важно в обосновании:

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

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

Это и есть правильный довод для такой работы: не «когда-нибудь будут пакеты», а «прямо сейчас перестанем пересчитывать доказанное».

Что отвергнуто и почему: Unison целиком — 15–25 тысяч строк, база данных вместо файлов, ревью без диффа. Слишком много и слишком рано.

Что взято как основа: Go с minimal version selection — простой и предсказуемый выбор версий, целостность по хешам. Ромб там решается подъёмом версии, и это честная, понятная людям схема.

Связано: names-not-hashes, what-goes-into-the-hash, unison-measured, content-addressing