Много думаю над тем, как продуктивнее всего обучить всем этим продвинутым темкам , чтобы в итоге научиться разрабатывать программы в парадигме топологически-ориентированного программирования (превращаем гомотопическую теорию типов в своеобразный DSL, язык "беспредеметной" области :)

Ежели по-взрослому, то это надо вдумчиво проходить несколько университетских курсов от хороших университетов из мировых топов.

А я хочу всё же попробовать обучить этому "наскоком", потому что всю математику под капотом тут знать в принципе не обязательно, если ориентироваться на некоторый условно прикладной уровень, потенциально доступный рядовому миддлу, который прошёл базовый курс по функциональному программированию. Немного похоже на машинное обучение: математики там тоже много, но чтобы начать создавать реальные проекты на DSL ML-фреймворков вроде PyTorch, всего-то надо пройти восемь ноутбуков моего курса например.
Что получится, не знаю, но если не попробовать , так и не узнать никогда.
Завтра выложу совсем простенький тренажёр по Martin-Löf Type Theory (альфа-версия).

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

В алгебре основное внимание уделяется операциям и свойствам этих операций: мы изучаем, как можно комбинировать различные элементы, и какие результаты мы можем получить. Геометрия же занимается изучением форм, их свойств и отношений между ними, и доказательствами различных утверждений в их отношении. И когда мы активно работаем с продвинутыми системами типов, то думаем примерно так, как будто в некотором смысле доказываем классические теоремы по геометрии (Curry-Howard correspondence в помощь).

То есть нулевой шаг пожалуй всё же будет изучать не алгебру и комбинаторную логику, а порешать задачки по геометрии, делая особый акцент на доказательстве теорем с большим количеством шагов доказательства. Сколь большим? Ну например доказательство Григорием Перельманом гипотезы Пуанкаре заняло около 200 шагов. А тибетские просветлённые мастера могли выстраивать логические цепочки длиной в несколько тысяч шагов.


Для разминки: задача об изогональных сопряжениях в треугольнике ABC. Пусть P — произвольная точка на плоскости снаружи треугольника, и не лежащая на его сторонах. Докажите, что существует случай, когда все три точки пересечения прямых PA PB PC со сторонами треугольника лежат на одной прямой (по теореме Паскаля о шестиугольнике). Помедитируйте сперва на визуальном решении.

Задачки Яковлева для школьников физмата и абитуры мехмата порешайте.

В любом случае, скилл длинных доказательств для программирования будет весьма полезным. Насколько полезным в сравнении с решением задачек на литкоде, погружением в реактивный фреймворк или шлифовкой прохождения собесов? Ну я не знаю. Мне просто это всё очень интересно, занимаюсь этим уже лет 20, и чем дальше, тем только увлекательнее. Вот и пишу об этом.