Из комментов, про HoTT

[akuklev]

Из комментов, цитата 1: «В смысле "когда RedPRL станет столь же удобен как ХХХ, то можно считать, что [..] применима в учебном процессе" - что здесь будет ХХХ?»

Такого XXX сейчас нет целиком, но можно собрать по частям.

Comments

[vit_r]

1. Стабильность, то есть устойчивость к ошибкам использования.
2. Наличие лучше оптимизированных под конкретный случай альтернатив.
3. Попытка сделать одинаково хорошо и человеку и компьютеру, причём, для совершенно разных по качеству задач.

[clayrat]

RedPRL кстати забросили окончательно, если куда и будут впиливать XTT, то в redtt.

[chaource]

Разработка визуальныхъ средствъ - дѣло дорогостоящее и занимающее многiе годы, пока не будетъ найдено удобное рѣшенiе. У меня есть небольшой опытъ работы съ Coq, а также нѣсколько лѣтъ опыта созданiя интерфейсовъ iphone, android, chromebook, web. Это долгая и кропотливая работа по отладкѣ каждого чиха пользователя въ каждой возможной ситуацiи. Созданiе графической программы, правильно показывающей интерактивную работу съ Coq и подсказками облегчающая поискъ доказательства (скажемъ, списокъ уже доказанныхъ теоремъ или функцiй съ авто-поискомъ по типамъ), займетъ не меньше полугода. Кто и когда будетъ этимъ заниматься, за какiя деньги? Наймите студента, пусть сдѣлаетъ это вамъ, если есть на грантѣ средства. Послѣ полугода работы, студентъ выдастъ результатъ, который будетъ работать на android, но пользоваться имъ для работы съ Coq будетъ менѣе удобно, чѣмъ emacs съ примитивной системой изъ трехъ буферовъ.

[nponeccop]

> Чтобы можно было прочитать курс матанализа не на базе теории множеств, а на базе какой-то теории типов,
> нам нужно чтобы эта теория типов была вычислительной

Ну HoTT-book написан не на вычислительной теории, в стиле Бурбаков. То есть в принципе можно хоттбук расширить, да и всех делов.