*cs

coq / ocaml = ocaml / c
крыша едет точно так же, как 10 лет назад от изучения функциональщины.
кстати, по "coq "program framework"" (собственно для написания кода, а не для доказательства) ищется слишком мало всего. Понятно, что фишка новая, но где про неё читать — ума не приложу. Есть идейки?

#ostnnh

13 comments

gadt'ы — только для typed [e]dsl evaluation
dependent types — только для проверки границ массивов
дискасс блеять.

#osofnz

7 comments

вопрос про пользу зависимых типов: http://gds.livejournal.com/63409.html — покаментите, если есть мнение. (тут или там — пофиг.)

#osofez

add comment

Как-то мне попалась в руки хорошая папира, хоть и от microsoft research, про "eventually consistent transactions": http://research.microsoft.com/pubs/15763...
И довольно удачно, потому что в работе подобное пригодится, вероятно.
И вот, дошли руки прочитать. Отзыв писал другому человеку, но ... more →

#oinhtf

2 comments

подумалась тривиальщина, по цепочке размышлений "бит → пол-бита".
по идее, пол-бита — это знание какого-либо факта с вероятностью 1/sqrt(2).
а есть ли какие-нибудь другие полезные штуки от представления вероятностей в битах, кроме всяких там шеннона и арифметического сжатия?

#oisoho

13 comments