>А сложность в том, что классический матан неконструктивен очень сильно, а первое пригодное для нормальной конструктивной теории определение вещественных чисел появилось всего-то четыре, что ли, года назад. Причём работает только в рамках HoTT, делать которую вычислительной научились всего год назад, и не самым элегантным образом (кубическая теория типов, причём её крайне нетривиальная разновидность). Ещё из общих соображений понятно, что там должен работать Propositional Resizing и Judgemental K для обыкновенных индуктивных типов (которые не "высшие"), однако никакого языка, который бы это прямо сейчас умел не существует. Короче это Cutting Edge исследований. >Про то, как работать с вещественными числами, в целом надо читать в https://homotopytypetheory.org/book/ и https://arxiv.org/abs/1610.05072, последнее — довольно новая статья, там более новые результаты и проявлена связь между полуразрешимыми предикатами на вещественных числах (соответствуют открытым множетсвам) и тьюринг-полнотой/частично-вычислимыми функциями (http://www.cs.nott.ac.uk/~psztxa/publ/fossacs17.pdf, http://www.cs.bham.ac.uk/~mhe/papers/partial-elements-and-recursion.pdf).