В хеш входит контракт, но не доказательство — у теоремы свой адрес

Ответ на вопрос, которого нет в литературе по адресации по содержимому.

Как у Unison: в хеш входит тело плюс объявленный тип. Документация и тесты — нет, у них свои адреса и ссылка на функцию.

Что из этого следует для flang. У нас у функции есть больше, чем тело и тип: постусловие, объявленная мера убывает, теоремы. Разделять надо так:

• постусловие и мера входят в хеш — это часть контракта. Функция с другим постусловием обещает другое, значит это другая функция, даже если тело совпадает;
• теорема в хеш не входит — у неё свой адрес и ссылка на функцию. Одну и ту же функцию можно доказать разными способами, и доказательство не должно менять её идентичность.

Красивое следствие, которое даёт эта схема. Если два разных адреса вычисляют одно и то же, это можно доказать и записать теоремой — отдельным объектом, связывающим два адреса. То есть «эти две функции равны» становится таким же гражданином базы, как сама функция.

Самое опасное место — не теоремы. У flang есть вещи, о которых легко не подумать при хешировании: четыре поверхности языка (одна и та же функция, записанная русскими и английскими словами, — одна функция или разные?), пределы шагов, объявленные коды отказов.

Связано: names-not-hashes, hash-inside-names-outside, content-addressing