.

Развиваю импортозамес и техноcуверен: пишу русский теорем-прувер с Z-типами.

Российских миллиардеров в Forbes полно, а я такой один.

Десятки миллионов евро, которые INRIA и евроуниверы вкладывают в Rocq на базе Calculus of Inductive Constructions (а Пентагон -- в Lean) -- это уже детский сад аспирантские штаны на лямках.

Переиграть и уничтожить.

За 2 часа и 15 долларов с Клодом4 я запилил всю эту хвалёную французскую петушатину CoC за 70 (семьдесят) строк кода на F# (+ вся мощща .NET прилагается).
Идеально для обучения, сделаю следующим гайдом по HoTT, перед "кубиками". В принципе, всего Барендрегта надо будет со временем запилить.