Узкоспециальное

[66george]

Я понял, чем мне не нравится деятельность вокруг HoTT, помимо общей странности затеи (испортить теорию типов гомотопиями). Это уже совсем не похоже на фундаментальную науку! Идёт некоторая инженерная деятельность, вроде "создания языка Go" (но создатели Go и не претендуют на большее). К Воеводскому как раз претензий нет, он доказывал теоремы о гомотопиях и проверял их пруфчекером, а вот вся орава, что за ним бросилась, или слегка одурела, или преследует коммерческие цели, одно другому тоже не мешает.

Comments

[russhatter.livejournal.com]

Я до какой-то степени понял, что хочет сказать rdia, и на фига инженерам нужно что-то на тему, которую Вы считаете своей (это я с намёком на то, как её могут уделать при случае).
Но пока понять-то я понял, а вот шевелиться в эту сторону нет. В-общем, когда-нибудь пойду копать...

[66george.livejournal.com]

А что хочет сказать rdia? В журнале rdia три открытых записи (все про школьные учебники)

[russhatter.livejournal.com]

http://russhatter.livejournal.com/251481.html?thread=4242265#t4242265
Вот. Собственно, флейм просто от Вашего коммента. И подразумевает ваши с ним выяснения отношений про Ваш учебник. Я из него понял для меня существенное. Совершенно не уверен, что из этого обсуждения Вы сами хоть чего-то можете вынуть: сказано всё на некотором языке, с которого нужно переводить. Если/когда буду копать - постараюсь, но тяжко, сейчас не до того...