Home
кококо
coq@conference.jabber.ru
Суббота, 3 января 2015< ^ >
zert установил(а) тему: кококо
Логи: http://chatlogs.jabber.ru/coq@conference.jabber.ru/
http://www.cis.upenn.edu/~~bcpierce/sf/ годная книга, как и всё, что пишет Пирс. Упор на тактики и доказательства.
http://adam.chlipala.net/cpdt/ годная книга. Доказательств мало, программирования много.
http://www.labri.fr/perso/casteran/CoqArt/index.html просто годная книга.
Конфигурация комнаты
Участники комнаты

GMT+3
[02:51:48] ForNeVeR вышел(а) из комнаты
[03:16:37] f[x] вошёл(а) в комнату
[05:28:59] f[x] вышел(а) из комнаты
[08:12:10] f[x] вошёл(а) в комнату
[09:40:02] f[x] вышел(а) из комнаты
[13:14:55] ftrvxmtrx вышел(а) из комнаты
[13:21:17] ftrvxmtrx вошёл(а) в комнату
[13:52:27] gds вышел(а) из комнаты: Replaced by new connection
[13:52:29] gds вошёл(а) в комнату
[16:51:39] <ForNeVeR> А в coq есть какой-то аналог сишного assert?
[16:52:04] <ForNeVeR> Ну вот я пишу функцию и тест-кейсы для неё. Как мне их описать, чтобы программа упала, если они выдают неверные результаты?
[16:52:54] <ForNeVeR> Сейчас я просто пишу Eval compute in my_func 1, а потом вручную сверяю результат с правильным. Но это ж я просто по глупости так поступаю, на самом деле должны быть нормальные способы ._.
[17:12:36] ForNeVeR вошёл(а) в комнату
[17:15:30] ForNeVeR вышел(а) из комнаты
[17:19:46] ForNeVeR вошёл(а) в комнату
[17:20:45] ForNeVeR вышел(а) из комнаты
[17:27:13] <gds> ForNeVeR: можно сделать Goal my_func 1 = 123. reflexivity. Qed.  --  если оно не равно (и это не доказывается тривиально), то оно не докажется.  Будет явная ошибка.
[17:28:35] <gds> конкретные примеры типа my_func 1 -- это иногда нужно, но ещё лучше -- доказывать какие-то свойства про функции.  Типа "для любых .. верно, что my_func 1 ..".
[17:39:49] <ForNeVeR> С этим я согласен, но у меня пока что по методичке задания попроще :3
[17:40:07] <gds> оппа, какая такая методичка?
[17:40:30] <ForNeVeR> Собственно, делаю упражнения из programs'n'proofs, на который тут недавно ссылку давали.
[17:40:57] <ForNeVeR> http://ilyasergey.net/pnp/ - this.
[17:41:09] <gds> а, я думал, что в учебном заведении такое преподают.
[17:42:27] <ForNeVeR> Я сам уже преподаю :3
Правда, не по компьютерной тематике.
[17:42:42] <ForNeVeR> И не про coq, разумеется. Просто преподаю.
[17:43:23] <gds> понял.  Интересно, что именно преподаёшь, но, если личное, то не надо.
[17:45:27] <ForNeVeR> Электродвигатели преподавал, пока был в аспирантуре. Сейчас отпуск на семестр взял. Вот диссер допишу и буду всякое про электромагнитные поля рассказывать.
[17:50:16] <ForNeVeR> А вот, между прочим, на соответствующих специальностях в вузе разве не изучают coq или что-то того же уровня?
[17:50:34] <ForNeVeR> И какие, интересно, специальности соответствуют? :)
[17:55:57] <gds> насколько я знаю про россию, только редкие вузы продвинулись даже до простой функциональщины.
[17:56:22] <ForNeVeR> Да ну, функциональщину у всех, по-моему, читают. Другой вопрос - в каком виде это делается.
[19:51:49] <aleksey> а вот и не у всех
Powered by ejabberd Powered by Erlang Valid XHTML 1.0 Transitional Valid CSS!