flang компилятор доказывает, что программа не зациклится 0.6.2 GitHub

Адресация по содержимому: версий нет, есть хеши

Идея владельца («библиотека Борхеса») совпала с устройством языка Unison: имя функции — хеш её собственного текста.

обычный мир
  myapp → библиотека A → json 1.2
        → библиотека B → json 2.0
  Конфликт: какую версию ставить? Одна из библиотек сломается.

адресация по содержимому
  myapp → библиотека A → #a3f9c2e1   (функция разбора, вот эта)
        → библиотека B → #7b0d4e88   (другая функция разбора)
  Конфликта нет. Это две разные функции. Обе лежат рядом.

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

Следствия: версий нет, конфликтов зависимостей нет, откат бесплатен, пересборка не нужна (тот же хеш → тот же результат). Минусы: имена для человека нужны отдельным слоем; нужно место под хранилище.

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

Открытый вопрос, которого нет в литературе. Входят ли в хеш постусловия, теоремы и объявленная мера? Если входят — доказательство привязано к телу навсегда (скорее хорошо). Если нет — надо решить, что значит «та же функция».

Проверено, и гипотеза в главной части не работает — но не из-за хешей: импорт сливает всё в плоское пространство имён, поэтому две версии не слинкуются при любой схеме адресации. См. names-not-hashes. Сам Unison измерен прогоном, и ромб он решает не так, как обещает лозунг — unison-measured.

Что взято из идеи. Хеш содержимого как идентичность внутри, имена и версии как интерфейс снаружи — hash-inside-names-outside. И ответ на вопрос про хеш: what-goes-into-the-hash.

Связано: owner-decisions, goal-of-the-language