Обещанное продолжение по HoTT ❤️❤️❤️
Но сперва небольшое отступление.

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

ТОП (топологически-ориентированное программирование)
(пока подобного термина нигде не было)

PHPoTT (моя программная реализация ТОП) -- это такой игрушечный функциональный язык с зависимыми типами, который однако умеет мощные штуки: прежде всего это явная работа с гомотопическими путями и высшими индуктивными типами.
Ну, да, нечто подобное по-взрослому умеют кубическая Agda, Arend, Coq с HoTT, Lean... Хотя нет, экспериментальная поддержка HoTT была в Lean 2, начиная с Lean 3 от HoTT отказались в пользу классической математики, а текущий Lean 4 вообще практически полностью сфокусировался на формализации обычной математики.

...В смысле? Разве HoTT -- это не "обычная математика"?
Нет, не обычная )

В "обычной математике" фундамент -- это абстрактная теория множеств, дискретность и статичность, а главное, сами доказательства -- это внешние по отношению к объектам конструкции. А HoTT -- про динамическую природу типов и конструктивные доказательства сами как объекты первого класса.

=

В ряде деталей PHPoTT обходит вышеупомянутые языки и пруверы. Ну например, конечно, тому же языку F* в целом прилично проигрываем, но...
В F* абстрактные refinement types, а у меня конкретные реализации высших индуктивных типов. В F* сложная система эффектов: они там первоклассные сущности в системе типов, и каждая функция должна явно декларировать, какие побочные эффекты она будет "производить" :) Хочешь исключение выбросить? Ставь ручками метку Exn. Надеешься, что чистая тотальная? Ставь Tot. И т.п. А PHPoTT -- простая система с явными гомотопическими путями.

=

Да, но "а что это всё вообще кому-то даст на практике??"

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

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

3. Мы также можем строго доказывать эквивалентность различных представлений криптографических структур :) включая формальную верификацию свойств "гладкости" криптографических функций. Формально описывать криптографические протоколы с сохранением их топологической структуры с верификацией свойств безопасности на уровне типов.
Получаем формальные гарантии безопасности,
верифицируем протоколы математически,
имеем возможность доказательного композирования криптографических примитивов,
получаем дешёвые и простые готовые инструменты для анализа устойчивости криптосистем,
и т.п. и т.д.
(картинки - это реально работающий код, шаблоны для конкретных задач, а не просто набранный в редакторе для демонстрации :)

Представляете, когда я обучу вас легко и просто подобным формальным подходам, которые сейчас и близко никто не понимает и не представляет (они даже не знают, что они этого не знают:)? С совершенно конкретным скиллом применения этого в вашей повседневной работе! 💪🏻💪🏻💪🏻💥💥🚀🚀🚀
(если конечно не релоцируюсь:)

Продолжение по курсам 3.0 следует; в следующий раз, как обещал, конкретно про самостоятельное начальное обучение этому напишу (сперва конечно надо в голову встроить соответствующую думательную машинку).

/dev прогресс по курсам 3.0: 23% => 27%
...
2. Фреймворк курса: 0% => 15%