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

[asviraspossible.livejournal.com]

Список авторов впечатляет...

[kurilka.livejournal.com]

Ты драфт не читал чтоли?
http://haskell.org/haskellwiki/Simonpj/Talk:FunWithTypeFuns

[nivanych.livejournal.com]

> enough fooling around: just use Coq

Глядишь, люди и прислушиваться начнут ;-)