>>122650
Есть, конечно, вероятность, что Стивен подберет однажды такой набор правил, чтобы сгенерировать точно такие законы как в нашей Кеноме, это было бы феноменально. А пока приходится довольствоваться гомотопической теорией типов HoTT, которая авторитетная и популярная, передний край академической науки, финансируется ведущими университетами. Владимир Воеводский медаль Филдсовскую получил за это. А его ученик Мэттью Уивер сделал UniMath. Владислав Бережок, Сергей Иванов, Валерий Исаев, Андрей Родин, Крис Капулкин, Эгберт Рийке, Гийом Брюнери, Андрей Суслин, Иван Панин, вроде все? Валерия Исаева особо отметим, он проклял российскую пидорскую агрессию и уехал в Европу. В гототопической теории типов получается оригинально: объекты это типы данных, а доказательства это программы, при этом основной тип это геометрическое пространство, а доказательство равенства двух элементов это непрерывный путь, соединяющий две точки. И доказать, что два доказательства равенства эквивалентны - это значит провести деформацию (гомотопию) одного пути в другой. Прикольно, что HOTT начали использовать в том числе и как описание Рулиады (!) - потому что теория типов идеально подходит для правил перезаписи этих графов Стивена. Переход от дискретных вычислений автоматов к непрерывному физическому пространству (а там и геометрии и гравитации) математически будет именно через высшие гомотопии (пути над путями). То есть HOTT это более общая и универсальная платформа, а Рулиада - это частный случай, частная модель. Хотя можно и наоборот сказать. Что Hott это вложение в Рулиаду, если по формальному определению следовать. И самое центральное это аксиома унивалентности.