to post messages and comments.

Привет, чятик! Общеизвестно, что эрланг, с точки зрения теории типов и прочего матана, довольно поганенький язык, на котором надоедает писать после полугода активного использования. Поэтому последнюю неделю я активно ковырял широко известный в узких кругах экстрактор CoreErlang github.com для Coq. Так вот, оно риальне работает. С некоторыми ограничениями, конечно, но работает.

Coq

Xenius: Так объясните, что хорошего в Coq? Ну то есть если там нельзя даже hello world вывести... что в нём можно делать?

Xenius: окамл диалект лиспа?

Xenius: Это Scala — диалект лиспа, который компилит в JVM

zert: давайте вконтакте паблик COQ создадим?

Это и многое другое ждет вас в гламурном чятике coq@c.j.r

<gds> проверка императивного алгоритма буферизованного чтения: gds.livejournal.com (Coq, OCaml)
<f[x]> "тогда я взял coq"
<gds> и твёрдо сжал его правой рукой.
<gds> после нескольких несложных действий я понял, что всё реально, всё в моих руках, и конец будет достигнут.

chatlogs.jabber.ru