спрашивал в камлочятике, но спрошу и тут.
У кого-нибудь есть желание и возможность совместно поработать над типизированной императивщиной для atmega-подобных мелочей в рамках coq? Нужен в том числе опыт писания под эти или подобные мелкие процессоры. (если не знаете coq, но владеете функциональщиной — заодно изУчите его, полезно всяко.)
Ну, понятно, @nicka уже неявно вписался в это мероприятие, но со стороны дизайна, а не со стороны кодинга, а я, боюсь, кодинг сам ниасилю. Но enjoy nih надо ведь!
Про сишечьку, плюсеки и прочие gcc-avr даже не упоминайте, это не торт.

#oegefo

3 comments recommend bookmark subscribe