to post messages and comments.

Короче, чувак, занимающийся зависимыми типами и доказательствами теорем, говорит, что надо писать тесты и делать код ревью. Шах и мат.

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

Coq

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

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

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

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

Это и многое другое ждет вас в гламурном чятике [email protected]

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

chatlogs.jabber.ru