(no subject)
Apr. 20th, 2016 12:36 am![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
66george
Visual Studio спрашивает "Готовы к переходу в облако?" Нет, спасибо, хочу ещё пожить.
Осваиваю психоделический пруфчекер Globular (на картинке). Теоремы (из теории категорий) изображаются психоделическими картинками, доказательство устроено по принципу "раскрась сам". Вот и для теории типов надо тоже так придумать. Вот Globular
https://golem.ph.utexas.edu/category/2015/12/globular.html
и статья про психоделические картинки, без которой ничего понять не удастся (не обещаю, что с ней удастся)
http://arxiv.org/pdf/1401.7220v2.pdf
