Namdak Tonpa (maxim) wrote,
Namdak Tonpa
maxim

Рантайм библиотека на Coq

Одно из заданий диссертации, построение рантайм библиотеки компактнее всего можно сформулировать вот так:

CoREPL> spawn ack 4 1
20
CoREPL> spawn ack 4 1 
21
CoREPL> ls
[(20,ack,10043),(21,ack,10033)]
20:65533
21:65533
CoREPL> kill 20
Ok
CoREPL> send 20 "hello"
Error
CoREPL>


Вот такое написать — уже неплохая цель, думаю даже больше будет чем любые другие а ля VM на Coq. Странно конечно звучит писать обычные программы, а в полях держать поля username и password в теоремах, но почему нет?

В такое я думаю трансформировать со временем https://github.com/5HT/co
Кто там хотел в Групоид Инфинити, приходите писать на Coq будет весело https://gitter.im/groupoid/exe
Денег нет, популярности нет, чистейшее R&D под ваши нужды, предлагайте свои идеи, будем в эту сторону двигать! Область наших интересов в этом проекте: стрим процессинг, векторизация, стрим фьюжин (т.е. с вероятностью > 1/2 то же, чем вы занимаетесь у себя на производстве) компиляция в LLVM языки — точка соприкосновения с http://groupoid.space/hnc. Этот проект назовем в будущем условно co — такого двухбуквенного сочетания в домене проектов нашей вселенной Marvell еще не было — REPL интерпретатор и рантайм система для программирования на Coq.
Tags: cs
Subscribe
  • Post a new comment

    Error

    Comments allowed for friends only

    Anonymous comments are disabled in this journal

    default userpic

    Your IP address will be recorded 

  • 0 comments