Поставил MAX, на уже совсем ближайшее грядущее будущее (хорошо ещё что не баклажан на фоне; что это вообще за масонская символика? :).

Закончил второй гайд "гомотопической теории типов для программистов", осталось на сервер выложить и потестить, в заключение добавил хардкорные тесты, думал не прокатят, но сработало, даже сам удивился 🤘

и дальше будет третий гайд "кубики" - кубическая теория типов, по заветам военных заказов Пентагона
"...extending the original foundational system of Homotopy Type Theory by enhancements based on cubical methods from algebraic topoology in order to make the resulting system more algebraic, and thus more computationally tractable".

В качестве примера думал сделать например абсолютно защищённый + формальный верифицированный мессенджер, в тему зачитался, смешное
"История о том как абсолютное оружие оказалось никому не нужным"

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