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

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