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

Развилки, которые владелец выбрал сам

Записано, чтобы не переигрывать заново и не «улучшать» молча.

Список объявлен суммой типов. Вопрос стоял так: приписать в начало должно быть постоянным по времени, как в Elixir и Coq, а не линейным. Решение — сделать список настоящим индуктивным типом.

Равенство морфизмов — через сетоиды. Из трёх подходов выбран первый: категория объявляет своё отношение на значениях объекта, равенство стрелок выводится поточечно. Отвергнуты типы тождества (нужны зависимые типы) и нормализация (годится лишь для узкого класса категорий).

Три типа чисел с разными гарантиями вместо одного — см. three-number-types.

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

Ветки сводятся в одну. Их набралось за двести; свод собирается отдельной веткой, потом перематывается main.

Тег и публикация — кнопка владельца. Действие необратимо, агенты его не делают.

Связано: what-is-deferred, write-in-plain-language