Ну, с Днём Науки!!1

Так-то вчерашняя победа над очередными "топовыми" версиями нейронок возникла вот из этих размышлений =>

У нас есть структурно разные реализации стека -- с помощью динамического массива, и с помощью связного списка. Но после того, как мы их "компилируем" в общую алгебру C[G] - интерфейс/абстрактный класс - они становятся неразличимы (изоморфны как алгебры), хотя и имеют разные вычислительные свойства.
Об этом же говорит и унивалентность в HoTT: критичным будет выбор эквивалентности типов. Если она будет слишком грубой, то у нас склеятся типы, которые склеивать не нужно.

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

...Да, но как формализовать важность доменных различий?

Нам нужно проектировать такими функторами, которые будут одновременно верны, полны, и отражают изоморфизмы!
Это именно та ключевая эквивалентность из HoTT: домен и код выражают одно и то же, 1:1, без потерь информации и без лишнего мусора.

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

Но ведь все эти моменты мы вполне можем формализовать!

...Думаю вот, а не сделать ли такой мета-фреймворк для AI, который вообще уничтожит всё человеческое программирование? :)

Или всё же лучше подготовить условный "гайд", который сделает только его владельца x100..x1000...x1000000 -кратным эксклюзивным программистом? А саму мета-методику хранить в тайне, и доверять лишь избранным ментатам, как Бене Гессерит :)

А то вы так и будете бесконечно "прописывать скиллы для агентов" с кучей топологических дыр.

Правда, для использования только самого гайда потребуется PhD в теории типов, но это, на мой взгляд, вполне достойный порог входа для подобных целей (+ я вам дам прямую тайную тропку к цели:).
...В любом случае, в конечном итоге в айтишке останутся только такие.

Impossible? Like that would stop me.