По направлению к COQ'у
Jun. 19th, 2009 09:00 pm![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png)
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.
Хорошее, годное замечание.
no subject
Date: 2009-06-20 07:04 am (UTC)