кстати, я и не убеждал насчёт "наше всё". Просто вот мне удобнее так. А когда обязан писать чистый код на coq — ругаюсь матом, беру свои манатки (как-то однажды сделал), и плачу, и колюсь.
там есть такая штука, что те, кто варятся в этом, уже знают какие-то вещи, а те, кто только начинает изучать, этих вещей не знает, и для него всё кажется убогим — и стандартная библиотека, и система сборки, и отсутствие пакетного менеджера (типа кабала) — при том, что всё это вполне таки есть, и расширения stdlib (аж два), и сборка нормальная, и пакетный менеджер.
Аа, это всегда с удовольствием, спасибо. У меня скорее вопрос по каким книгам учить Coq (calculus of inductive constructions?).
p.s.: но до окамла я всё равно не знаю когда доберусь, т.к. во-первых хаскель не домучал, а во-вторых возьму си и сетевое программирование какое-нибудь до него, т.к. стыдно не знать
Coq — "петух" по хвранцузски. Но там унутре CIC, факт. По каким книгам — есть варианты. По ответам на вопросы я подберу: - для каких целей собираешься использовать coq? Либо доказательства теорем с формальной проверкой, либо программирование с кошерными типами. - функциональщину умеешь более-менее ок?
сетевое программирование можно и на окамле, в каменте у амд63 была ссылка на документацию на модуль Unix — его много где хватает. Конечно, если ручками пакетики собирать — тут уж хуюшки. Я просто не читал ту книжку, про которую ты недавно писал.
Да, собственно, никаких целей нету — просто хочется матчасть иметь хоть какую-то по доказательствам теорем, что это и как можно применять (про кошерные типы я вообще не очень понимаю что к чему).
Про функциональщину — ну тоже, смотря что имеешь в виду. В целом — да, умею, SICP читал и понимаю, х-ль немного пишу тоже.
Писать, естественно, реальные (сложные) программы на си не собираюсь, а вот как минимум для тестов разных нагрузочных (ну, или прочих, требующих извращений) кто как не он.
тогда можно взять камло, C, сетевое, и вперде. Только вот, узнав, как делаются биндинги для окамла, и посмотрев на х-евые, у многих людей возникает тошнота. Если в будущем будешь использовать х-ь плотно, тошнота нежелательна. Кстати, с биндингами поможем — @ygrek (и в камлочятике еть) пса на них съел, да и я ещё помню многое.
доказательства теорем — интересная штука, стоит изучить. Только затягивает, сцука такая.
кошерные типы — ну, например, классика: вектор ( = список с количеством элементов в типе). Для него функция склейки имеет такой тип (где A — тип элементов вектора):
forall A n m, vec n A → vec m A → vec (n + m) A
Ничего необычного не видишь? (хотя на практике векторы не очень нужны. Но представление о зависимых типах дают. Эдакий "факториал".)
Итак, на основании ответов советую http://adam.chlipala.net/cpdt/ (первую главу, чото там про стек, просто просмотри, не вникай). Если окажется сложно — откатись на "software foundations" и пробуй их в параллель. Но лучше бы не оказалось — во второй книжке много воды.
По coq помогу, простые вещи уж точно. Если не смогу — есть #coq irc и официальная рассылка coq-club, там добрые, но англоязычные.
а тесты — и на окамле можно, если не нужно каждый такт выжимать. Окамл очень тупой в плане компиляции, выжать можно много. Однако я прекрасно понимаю, что иногда си незаменим.
17 comments
recommend
bookmark
subscribe
ping
хмм, значит работает. А к #tsfgse/22 ответ не могу добавить — так вот как он работает, этот блеклист ваш
кстати, я и не убеждал насчёт "наше всё". Просто вот мне удобнее так.
А когда обязан писать чистый код на coq — ругаюсь матом, беру свои манатки (как-то однажды сделал), и плачу, и колюсь.
ну, я просто хотел выразить своё желание следующим таки попробовать OCaml, тут "наше всё" без сарказма.
там есть такая штука, что те, кто варятся в этом, уже знают какие-то вещи, а те, кто только начинает изучать, этих вещей не знает, и для него всё кажется убогим — и стандартная библиотека, и система сборки, и отсутствие пакетного менеджера (типа кабала) — при том, что всё это вполне таки есть, и расширения stdlib (аж два), и сборка нормальная, и пакетный менеджер.
то есть, я к чему: если будут какие-то вопросы — спрашивай их в псачике или в ocaml@conference.jabber.ru.
Аа, это всегда с удовольствием, спасибо. У меня скорее вопрос по каким книгам учить Coq (calculus of inductive constructions?).
p.s.: но до окамла я всё равно не знаю когда доберусь, т.к. во-первых хаскель не домучал, а во-вторых возьму си и сетевое программирование какое-нибудь до него, т.к. стыдно не знать
Coq — "петух" по хвранцузски. Но там унутре CIC, факт.
По каким книгам — есть варианты. По ответам на вопросы я подберу:
- для каких целей собираешься использовать coq? Либо доказательства теорем с формальной проверкой, либо программирование с кошерными типами.
- функциональщину умеешь более-менее ок?
сетевое программирование можно и на окамле, в каменте у амд63 была ссылка на документацию на модуль Unix — его много где хватает. Конечно, если ручками пакетики собирать — тут уж хуюшки. Я просто не читал ту книжку, про которую ты недавно писал.
ну, как "хуюшки", можно, но оно тебе будет неинтересно, эти биндинги писать.
Да, собственно, никаких целей нету — просто хочется матчасть иметь хоть какую-то по доказательствам теорем, что это и как можно применять (про кошерные типы я вообще не очень понимаю что к чему).
Про функциональщину — ну тоже, смотря что имеешь в виду. В целом — да, умею, SICP читал и понимаю, х-ль немного пишу тоже.
Ну, мне как раз научиться си до уровня "понимать и уметь делать биндинги для всего" хотелось бы.
Писать, естественно, реальные (сложные) программы на си не собираюсь, а вот как минимум для тестов разных нагрузочных (ну, или прочих, требующих извращений) кто как не он.
тогда можно взять камло, C, сетевое, и вперде.
Только вот, узнав, как делаются биндинги для окамла, и посмотрев на х-евые, у многих людей возникает тошнота. Если в будущем будешь использовать х-ь плотно, тошнота нежелательна.
Кстати, с биндингами поможем — @ygrek (и в камлочятике еть) пса на них съел, да и я ещё помню многое.
Круто, спасибо)
доказательства теорем — интересная штука, стоит изучить. Только затягивает, сцука такая.
кошерные типы — ну, например, классика: вектор ( = список с количеством элементов в типе). Для него функция склейки имеет такой тип (где A — тип элементов вектора):
forall A n m, vec n A → vec m A → vec (n + m) A
Ничего необычного не видишь?
(хотя на практике векторы не очень нужны. Но представление о зависимых типах дают. Эдакий "факториал".)
Итак, на основании ответов советую http://adam.chlipala.net/cpdt/ (первую главу, чото там про стек, просто просмотри, не вникай). Если окажется сложно — откатись на "software foundations" и пробуй их в параллель. Но лучше бы не оказалось — во второй книжке много воды.
По coq помогу, простые вещи уж точно. Если не смогу — есть #coq irc и официальная рассылка coq-club, там добрые, но англоязычные.
> реальные (сложные) программы на си не собираюсь
рад.
а тесты — и на окамле можно, если не нужно каждый такт выжимать. Окамл очень тупой в плане компиляции, выжать можно много. Однако я прекрасно понимаю, что иногда си незаменим.