@s_ivanov боюсь, что код нам надо писать на PROMELA, а хаскель из него генерировать. ну либо писать его на ограниченном DSL и из него генерировать PROMELA и хаскель, ну или уж Си. чего уж там.

примеры я посмотрел...

что-то профита вижу мало. сейчас другие скину

1) тупо и просто: https://github.com/voidlizard/emufat/blob/master/src/CWriter.hs

тупо и просто два https://github.com/voidlizard/hopc/blob/master/src/Compilers/Hopc/Backend/TinyC/CWriter.hs

@voidlizard генерация префиксного дерева ещё используется у вас?

да

вот как раз примеры из неё ищу

ты там Leijen по моему использовал

угу

какой-то из pretty-printer-ов

language-c какой-то слишком замученный для этого кейса был и без документации почти

3) тоже не очень сложно: https://github.com/voidlizard/hctrie/blob/master/Language/C/Generate/Trie.hs

в общем-то, не очень ясно, зачем там что-то специальное, что бы си генерить

ну well-formed и все такое

если там сложный вложенный код, то смысл может быть

leijen это как раз решает

блоки, скобки

точки с запятой в конце блоков. но это и без него решается

про promela я подозреваю, если писать через какую-нить free структуру то проще из haskell генерить промелу

у нас кстати часть алгоритмов на промеле было моделировано

даже баги находились

я могу рассказать, как например для Сухого доказывают сишные модули при помощи промелы

но промела это ад какой-то, в is parallel programming hard and what we can do about it был пример мьютексов

как раз в ЦПИ сидели люди, которые на кафедре параллельно этим занимались, код для Сухого писали и доказывали

прикольно

корчое рассказываю

1) берешь студентов последних курсов и аспирантов

2) платишь им небольшие деньги

3) заставляешь брать сишный код и писать для него модель на промеле

4) профит

модельки там это ужас же

нужно или сильно моделировать, или убьёшься все эти эффекты в модель тащить

студенты и аспиранты никуда не денутся, опять же им деньги нужны

это да

особенно, если ты же их научный руководитель. и если они свалят с проекта, то защищаться будут потом всю жизнь

жестоко

но все же promela это исключительно на труде рабов, писать на ней в трезвом рассудке вроде мало кто захочет

ещё и кластер собирать с террабайтами памяти

=)

ну я понаслушался рассказов и даже смотреть не стал

крутой проект делали авторы Mirage OS

они сделали dsl для описания протоколов - как парсеров, так и FSM-ов

и для FSM-ов у них генерилась спека в PROMELA

почему они на это забили и все стеки напедалили прямо на raw окамле в итоге я понять не могу

было круто, а стало обычно. хотя реализация SSL/SSH на окамле все равно доставляет

угу, это действительно круто

у нас была штука со стейтмашинками, я хотел генерить промелу но так времени и не было

а вот такую тему видали? https://github.com/seL4/l4v

какая-то эпичная хрень воще

видали, да.

я пытался что-то понять, но тщетно

впрочем, я дальше доказательства законов функтора не заходил толком

у них haskell доказательства ещё поддерживаются, или целиком на isabelle?

ну у них тоже подход, пишем код - доказываем - конвертим (руками?) в си

почему они на это забили и все стеки напедалили прямо на raw окамле в итоге я понять не могу

Пришел менеджер и сказал "Нефик играться, надо показать рабочее".

какой менеджер в академии?

это университетский проект

но хотя менеджер который принудил всех писать на окамле вместо промелы это персонаж, достойный отдельного

Ну, научрук

Вот эва.

В целом метаописание протоколов вещь правильная. Но если глянуть в код стечков - там стока подпорок...

да ты вообще живые такие проекты видел?

Какие? С метаописанием?

Суриката.

Ну и asn1 еще не подох.

И ldap по нему генерится вроде как.

Но да, мало.

Ибо всегда есть нюансики.

верно вообщет

просто фб обычно не хайрит на конкретную позицию

и не факт что есть открытые позиции в этих командах прямо сейчас

@mkrentovskiy суриката это ж просто сигнатуры выделяет? что-то типа регекспы на стероидах?

вот небольшое подтверждение наличия сабжа в фейсбуке http://simonmar.github.io/posts/2016-12-08-Haskell-in-the-datacentre.html

и вот ещё https://code.facebook.com/posts/745068642270222/fighting-spam-with-haskell/

раскрываю, как сделать хаскел-в-почти-любой-компании: приходишь в компанию - в какой-то момент делаешь что-то на хаскелле - теперь в этой компании - хаскел в продакшоне (111)

в дойчебанке, например, был SML в продакшоне (111)

таким же ровно образом появился, как я только что рассказал. я его лично сам на перл переписывал, потому что sml-ный код надо было собирать по мануалу в шесть страниц A4

это нужно железные яйца иметь и достаточно высоко быть

лучше бы я его переписал на хаскелл, но я тогда (1) не знал таких слов (2) думаю, что ghc в той версии, которая была в том году, был немногим лучше sml