То странное чувство, когда последовал своим собственным рекомендациям из курса по вайб-проектированию, и вместо 100 долларов на первую неудачную итерацию теперь потратил всего 5, а получил полноценную реализацию первых базовых понятий CTT, причём с полного нуля и вдобавок с готовой спецификацией для последующей работы.

Клод4 затупил всего в двух тестах, и только в одном относительно серьёзно. Вообще уже не раз замечал, жпт начинают путаться, когда надо выполнить композицию различных сущностей -- например, при композиции кубов, двух систем по общим граням и т.п. (я специально решил сделать явный оператор композиции, который объединяет два куба вдоль общей грани, потому что это дальше будет база по композиции путей и для условия Кана).

И по мере того как изучаю это всё, открываются весьма неожиданные темки в плане применения движка HoTT+CTT: верификация квантовых алгоритмов в принципе ещё где-то на первых, поверхностных уровнях пространства понимания.

=

Как вам например такая задачка, как управление мегароем небольших дронов (размером с птицу). Сегодня мы видим сотни дронов, скоро счёт пойдёт на тысячи, в следующем десятилетии и на миллионы; ну в конечном итоге так-то точно и будет когда-нибудь.Засада в том, что такой миллион летающих роботов должен действовать как единый организм.

Вы же читали профильную классику -- "Непобедимый" Лема, "Рой" Стерлинга, "Муравьиная ферма" Фрэнка нашего Герберта? Ну вот она уже тут. По Лему кстати пару лет назад вышла шикарная игра "The Invincible", собравшая кучу призов.
(Кстати, а почему у нас игры по Беляеву например не делают? у него в книгах множество абсолютно уникальных идей; или Ефремов; я уж не упоминаю Б.С. ...)

Но структура такого мегароя -- не просто большое число, это качественно новый уровень сложности. В нашем мозгу всего-то 80+ миллиардов нейронов, но они не летают в трёхмерном пространстве и не рискуют столкнуться друг с другом на скорости 20 метров в секунду. Для сравнения, современный игровой движок даже просто коллизии простых сфер потянет, ну может сотню тысяч для нескольких тысяч объектов на кадр. А если меши, так вообще штук сто на 10 тыщ коллизий. А если continuous collision detection требуется?

Так-то каждый дрон может находиться в тысяче (порядок) различных состояний, и соответственно общее число возможных состояний мегароя составляет тысячу в степени миллион.

Никакая счётная математика это не потянет в принципе, здесь нужен на порядок более глубокий концептуальный уровень. На сегодня поможет в этом только гомотопическая теория типов.