gds
10.03.2012 13:38 umodniB2B586F5
coq / ocaml = ocaml / c
крыша едет точно так же, как 10 лет назад от изучения функциональщины.
кстати, по "coq "program framework"" (собственно для написания кода, а не для доказательства) ищется слишком мало всего. Понятно, что фишка новая, но где про неё читать — ума не приложу. Есть идейки?
13 comments
recommend
bookmark
subscribe
Чо, вставляет?
у меня пока "сбор впечатлений". В основном — какое-то охуевание по началу. Слишком много всякого разного. Даже мастера coq'а борются с ним по гуглу, что тут про меня говорить.
А, учитывая не лучшее физическое/интеллектуальное состояние, эффект потрясающий. Вставляет, то есть.
На "тактики" надо как-то забить, это какой-то ебучий forth, стековая машина с write-only кодом. Ищу, как грамотно писать код, пока ничего не нахожу.
Вот такой "дамп сознания".
Спасибо. Надо тоже покурить.
присоединяйся. Вместе веселее всяко.
Пока моя первая цель — сгенерить хелловрот в камлокод. Дальше — ygrek подкинул задачку про dht (kademlia), тоже хочется подёргать себе этосамое, но там массивы, сложнее. Либо как "аксиомы" их присунуть ("факты, которые не потребуют доказательств" — всякие Array.{make,get,set} так захуячить), либо ещё какое-то шаманство оформить. Не знаю пока.
Не, у меня сейчас говноработа, потом.
каких профитов хочешь достичь используя coq непосредственно для погромированния?
в основном хочу пощупать на практике зависимые типы. Хочу понять, как доказывать какие-либо утверждения _о программах_. (про просто доказательство всякого матана в coq — представление имею.) Хочу понять, где есть смысл в доказанном коде, а где нет. (то есть, сейчас я только примерно понимаю, но после личного опыта использования понимание будет точно глубже.) Хочу посмотреть, понравятся ли мне зависимые типы, и в каких именно областях понравятся.
Agda вроде попроще, потому крыша лично у меня не едет (и это я уже умею доказывать ассоциативность). но ощущения плюсую :)
agda попроще, да. Но вот начал читать http://adam.chlipala.net/cpdt/ и понял, что в coq есть свой прикол. Тем более, забавно иметь возможность кодогенерить как в камло, так и в хаскель.
А что решаешь на агде? Есть какие-нибудь мелкие, но прикольные задачки? Мне реально интересно, руки чешутся порешать (и порешить!111) их.
я пока учусь. надеюсь в ближайшее время записать базовую аксиоматику вещественных алгебр и попробовать подоказывать изоморфизмы вроде C+C ~ CxC. ну и категории — от леммы Йонеды на Isabelle у меня глаза вытекли, а на Agda вроде ничего, даже читаемо. посмотрим
в мире слишком мало людей, занимающихся agda/coq, которые "пока не учатся", это я знаю :)
А после вещественных чисел что? Есть реаллайф-применения, или просто интересно повертеть теоремки различные?
тьфуты. которые "_уже_ не учатся".
никаких. ну то есть идеи чисто по математике — вагон; а вот с реальными приложениями напряжёнка