книга -- это хорошо, но тут маловато будет. А вот сначала заточить coq до приличной экстракции всего, записи поправить, какую-нибудь шнягу для императивщины сделать -- и вполне можно. Но сложно. С другой стороны, я сформулировал фейлы, можно и на багтрекер набигать. А так, CPDT вполне таки описывает и вопросы экстракции тоже, просто не всегда явно, без рецептов "если хотите такой код -- делайте так-то".
Про dependent types -- там особо нет проблем, разве что доказательства. Проблемы же были в императивщине -- как и у любого чисто-функционального языка программирования. Вообще, решение манатками далеко не единственное, но мне не хотелось долбаться с неизвестным результатом, хотелось ожидаемый результат, а с манатками в окамле я умею. Да, императивщина -- ужос. Но далеко не всегда есть необходимость что-то в ней доказывать. Поэтому так и сделал: где основная "движуха", там императивщина, а где отдельные изолированные куски с гарантиями, там функциональщина.
> Computer science theorists реально вообще не интересуются практикой работы программиста?
интересуются, но на свой манер. В частности, после их исследований мало что может пригодиться без лишнего гемора для дел. Гемором этим может быть что угодно -- хоть и наладка "экосистемы" (как в случае с компиляцией в пределах окамловского проекта).
С другой стороны, я сформулировал фейлы, можно и на багтрекер набигать.
А так, CPDT вполне таки описывает и вопросы экстракции тоже, просто не всегда явно, без рецептов "если хотите такой код -- делайте так-то".
Про dependent types -- там особо нет проблем, разве что доказательства. Проблемы же были в императивщине -- как и у любого чисто-функционального языка программирования. Вообще, решение манатками далеко не единственное, но мне не хотелось долбаться с неизвестным результатом, хотелось ожидаемый результат, а с манатками в окамле я умею.
Да, императивщина -- ужос. Но далеко не всегда есть необходимость что-то в ней доказывать. Поэтому так и сделал: где основная "движуха", там императивщина, а где отдельные изолированные куски с гарантиями, там функциональщина.
> Computer science theorists реально вообще не интересуются практикой работы программиста?
интересуются, но на свой манер. В частности, после их исследований мало что может пригодиться без лишнего гемора для дел. Гемором этим может быть что угодно -- хоть и наладка "экосистемы" (как в случае с компиляцией в пределах окамловского проекта).
Reply
Leave a comment