>@gds банит на мертвом канале за ``оффтопик'' >@zert установил(а) тему: кококо пидорахи как всегда

где ваш php теперь? http://coq-blog.clarus.me/a-blog-engine-written-and-proven-in-coq.html

Читаю матан, вижу упражнение на доказательство для САМОПРОВЕРКИ. Решаю, решил неправильно/думаю, что решил неправильно. Лезу в ответы. Не нахожу (там ток СЛОЖНЫЕ). Понимаю что автор не рассчитывал, что его книгу будут читать такие имбецилы как я. ВНИМАНИЕ ВОПРОС Если я вкурю Coq (или че там щас модно), я смогу играть в математика? Или это по большей части дроч^Wборьба с типами, чем средство удобн^Wинтерактивного доказательства теорем?

http://homes.cs.washington.edu/~jrw12/dep-destruct.html -- грамотно про dependent destruction.

http://www.sendspace.com/file/4vtin4 Запись диалога знакомого в техподдержке с клиентом.