По направлению к 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

[nivanych.livejournal.com]

Там есть экспорт в хаскель,
так что, значительную часть
можно делать и на коке.
Но я не слышал, чтобы на нём
хоть кто-то делал прикладные программы...

[kurilka.livejournal.com]

Ну дык неудобно, видать, микроскопом гвозди забивать :)

[nivanych.livejournal.com]

Надеюсь исправить эту ситуацию.
Микроскоп должен быть удобным ;-)

[kurilka.livejournal.com]

эээ, ты меня пугаешь :)

[nivanych.livejournal.com]

Да не.
Так-то, сделать удобства типа
того же хаскелевого IO, библиотеки,
и уже вполне можно было бы
"промышленно" программировать на Coq.
Но мне больше нравится Agda.
Но в Coq с доказательствами лучше.
Хоть мне и не нравится способ,
которым они сделали улучшения.

[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".
Главное, чтобы для простых вещей
оно не становилось сложнее.