Опыт использования Coq на практике, или Как я сам себя отпетушил COQОКОКОКО

[gds]

Есть время собирать опыт.

Есть время разбрасывать на вентилятор.

Уже довольно давно система типизации в окамле кажется мне слегка недостаточной.

Comments

[maxim]

Ебануться.

[deni_ok]

познавательно

[kurilka]

познавательно

[chaource]

Чрезвычайно интересный обзоръ! Вообще-то, матерiала достаточно для книги на эту тему.

Я думаю, проблемы и трудности при использованiи dependent types - это проблемы перевода изъ, условно говоря, ассемблера на машинно-доказуемый языкъ. Императивщина, объекты, циклы - это очень плохая и сложная вещь, её очень трудно чётко понять и что-либо формально провѣрить. Пытаясь перевести это всё на Coq, мы какъ разъ и вынуждены взглянуть этому ужасу въ лицо. А pure functional paradigm достаточно простa и хорошa для пониманiя.

Понял многое про академоту.

А что именно? (Computer science theorists реально вообще не интересуются практикой работы программиста?)

[ext_1035828]

C-c-c-c-combo breaker!!111

[gds]

книга -- это хорошо, но тут маловато будет. А вот сначала заточить coq до приличной экстракции всего, записи поправить, какую-нибудь шнягу для императивщины сделать -- и вполне можно. Но сложно

[jakobz]

Ебануться.