ТОП - это когда мы не просто высокоуровневые спецификации (полученные например с помощью BDD) переводим в некоторый код (как сегодня фактически происходит во всём мировом программировании, от вайб-кодинга с околонуля до монадических механик на этих ваших хаскелях),
а с помощью абстрактных типов выражений (вычислений) задаём контракты для бизнес-логики, определяя ограниченное множество допустимых путей (в смысле гомотопической теории) в пространстве возможных/допустимых преобразований данных, которые вдобавок нам подсказывает смарт-редактор (такие обязательно появятся со временем, да и плагины можно делать к существующим).
Но главное, что мы таким образом задаём и правила композиции этих путей, что позволит проектировать логику системы как когерентное взаимодействие слоёв абстракций.
Модульность — через унивалентность (эквивалентность изоморфных структур).
Управление потоком вычислений -- через зависимые типы (как спецификации инвариантов).
Композиция эффектов — через transport along Path (согласованное преобразование контекстов): "переносим" значение из типа A в тип B с сохранением внутренней структуры, если задан путь (доказательство тождества) p : A = B.
Говоря по-программистски, гарантированно безопасное приведение типов.
Сложная логика — через высшие индуктивные типы (инкапсуляция состояний и переходов).
Например, тип List задаёт свободную алгебру над сигнатурой {nil, cons}, а его элиминатор -- рекурсивную схему, логически ограничивая допустимые операции.
Тип (как спецификация пути в ∞-группоиде вычислений) по сути автоматически "выбирает" код своей реализации!
=
Вообще, транспорт через тождества из HoTT (слоистая композиция через когерентные гомотопии, ну или аналог рефакторинга с гарантиями — как вам больше нравится :) -- это прям мощща (монадические bind + pure/return ушли курить далеко и надолго).
Гарантируем, что "побочные эффекты" не нарушают глобальную структуру (на уровне зависимых типов -- например, List -> Vector для конкретной длины).
А сами завтипчики (с продвинутым паттерн-матчингом) позволяют статически кодировать пред- и пост-условия (логика как доказательства), а унивалентность позволяет сменять реализации, сохраняя эквивалентность.
Короче говоря, тип f : (x : A) → B(x) в HoTT -- это не просто функция, а доказательство, что для любого x в A существует конструктивный метод получения B(x), встроенный в целостную гомотопическую структуру типов нашей системы.
Таким образом, подобная система типов становится метаязыком (MetaDSL a-la Math Wins по Алану Кэю) для проектирования логики, где программы -- это не наборы инструкций, а доказательно-топологические конструкции, формально управляемые правилами HoTT.
=
Мой прогноз: к 2030-му с развитием AI эти темки будут здорово распространены, а повседневное кодирование фактически канет в небытие. И соответственно порог входа в айтишку сильно вырастет, и даже знание функциональных языков уже особо не поможет. Ну научилась вы структурировать код с помощью хаскелевских категорий (которые просто инструменты), чуть повыше уровень абстракций для вчерашних Python-программистов с functools, и всё.
А HoTT -- это про формализацию математики: типы трактуются как пространства, а программы -- как доказательства теорем. И вот применительно к повседневному программированию тут открываются столь невероятно мощные и широкие пути, что я в процессе подготовки курса был просто поражён потенциальной мощью гомотопической теории 💥
=
Но мы на курсе это всё конечно разбираем очень-очень просто, без математической терминологии: просто пишем модель гомотопической теории на питончике с очень детальным разбором каждого момента, и понимание темки приходит естественно легко и просто. По сути
"К лету курс 💯будет готов."
Предварительный уровень? Ну вот кто прошёл успешно мои курсы "функциональное программирование на F#" и "солвер Z3 на Python", значит готов на 💯