приняли такое волевое решение.

С++ подходит.

а в какой сфере ты работаешь?

да, cblp пытался протолкнуть - но не получилось

а в какой сфере ты работаешь?

Image processing

а какие-то более безопасные языки нельзя использовать? раст какой-то?

не знаю как там не в large scale а на SKA вроде протолкнули haskell

надо с этими ребятами ещё поболтать

а какие-то более безопасные языки нельзя использовать? раст какой-то?

раст еще не production-ready, на мой имхо

ну у плюсов есть halide и т.п.

@anpryl чувак, который AJHC делал, писал довольно-таки хардкорный embedded

пока не устал

@voidlizard а чем ты кстати генерил C? свое писал что-то или пользовался какой-то либой?

мягкий эмбеддед - это какой-нить промконтроллер с Atom/Geode и 128M RAM. х-ль там работает аж бегом

Ребята, мне просто хочется поделиться этим. Почему хаскель. Цитирую Дейкстру. "Глубоко ошибается тот, кто думает, что изделиями программистов являются программы, которые они пишут. Программист обязан создавать заслуживающие доверия решения и представлять их в форме убедительных доводов, а текст написанной программы является лишь сопроводительным материалом, к которому эти доказательства применимы."

и на мипсе бы работал, и я бы не страдал, есл бы кто-нибудь написал бы нормальный бэкенд для мипса. я не могу

этим надо лет пять одному заниматься

если начать прямо сейчас. то через пять лет мипса на рынке останется 25% от сегодняшнего

@anpryl я генерил си при помощи Text.Printf но вообще есть всякие Text.PrettyPrint.Leijen что бы скобки закрывать и идентацию делать

я вот такое нашел https://github.com/ollef/Generate-C

Ребята, мне просто хочется поделиться этим. Почему хаскель. Цитирую Дейкстру. "Глубоко ошибается тот, кто думает, что изделиями программистов являются программы, которые они пишут. Программист обязан создавать заслуживающие доверия решения и представлять их в форме убедительных доводов, а текст написанной программы является лишь сопроводительным материалом, к которому эти доказательства применимы."

во времена Дейкстры все было иначе - тех же энтерпрайзов никто и представить не мог

@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 на окамле все равно доставляет

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

ERROR: S client not available

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

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

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

видали, да.

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

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

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

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

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

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

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

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

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

Ну, научрук

Вот эва.

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

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

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

Суриката.

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

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

Но да, мало.

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

Не в продолжения срача, но утветждение про хаскель в Фейсбуке меня заинтересовало и похоже оно не верно. Там была всего одна вакансия, да и то не для программиста на хаскель: https://www.reddit.com/r/haskell/comments/4zclkm/haskell_positions_at_facebook/

Не в продолжения срача, но утветждение про хаскель в Фейсбуке меня заинтересовало и похоже оно не верно. Там была всего одна вакансия, да и то не для программиста на хаскель: https://www.reddit.com/r/haskell/comments/4zclkm/haskell_positions_at_facebook/

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

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

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

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

Не в продолжения срача, но утветждение про хаскель в Фейсбуке меня заинтересовало и похоже оно не верно. Там была всего одна вакансия, да и то не для программиста на хаскель: https://www.reddit.com/r/haskell/comments/4zclkm/haskell_positions_at_facebook/

вот небольшое подтверждение наличия сабжа в фейсбуке 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