>>122652То есть Рулиада - это бесконечный ле, сама бесконечная Вселенная, а HoTT язык ее описания формализации, чтобы рисовать описывать траектории, пути и пространства внутри Рулиады, в частности все доказательства чего угодно должны быть выражены на языке гомотопий HoTT, тогда они будут формально строгие.
С другой стороны, по замыслу, по определению самому, Рулиада включает в себя вообще всё, что может быть вычислено, в том числе что особенно важно для ужас-треда и мистиков: Рулиада содержит нечеловеческую логику!
Там могут быть другие правила вычислений, чуждые нашему разуму, и даже наверное даже HoTT просто не работают в некоторых областях.
HoTT - это все-таки человеческий инструмент, а Вольфрам замахнулся на Запредельное.
Но сами же математики и физики (включая команду Вольфрама!) используют HoTT как фундаментальный язык программирования для описания Рулиады, вот такие дела.
Внутри Рулиады физический мир рождается из дискретных шагов вычислений, но если мы хотим математически строго доказать, как эти миллионы мелких вычислительных шагов превращаются в гладкое, непрерывное пространство нашей Вселенной, нам не обойтись без геометрии путей.
На самом деле всё придет к гипертьюринговым вычислениям, которые просто нереально выполнить на практике, потому что они требуют бесконечной энергии, бесконечного времени и бесконечной материи.