По направлению к COQ'у

[deniok]

Simon Peyton Jones, Chung-Chieh Shan и Oleg Kiselyov обещают статью "Fun with type functions", а пока выложили слайды. После впечатляющих примеров на Хаскелле с использованием индексированных семейств типов и функций над типами, радует замечание на последнем слайде:

At some point it may be best to say “enough fooling around: just use Coq”. But we aren’t there yet.

Хорошее, годное замечание.

Comments

[kurilka.livejournal.com]

Кстати, начал тут Фоккингу читать, дак он цитирует Хоара (ту работу я не смог нагуглить):
"Category theory is quite the most general and abstract branch of pure mathematics. [ . . . ] The corollary of a high degree of generality and abstraction is that the theory gives almost no assistance in solving the more specific problems within any of the subdisciplines to which it applies. It is a tool for the generalist, of little benefit to the practitioner [ . . . ]."

[nivanych.livejournal.com]

Может и так.
Но чем сложнее задача,
тем выше уровень "generality".
Главное, чтобы для простых вещей
оно не становилось сложнее.