?

Log in

Дважды мудак [entries|archive|friends|userinfo]
Декларативное рулит

Site Meter

[ website | Мой сайт ]
[ userinfo | livejournal userinfo ]
[ archive | journal archive ]

Экстракшен [мар. 25, 2017|23:05 pm]
Andy Melnikov
[Tags|, , ]

https://hal.archives-ouvertes.fr/file/index/docid/338973/filename/letouzey_extr_cie08.pdf

Долго длившийся односторонний "спор" с maxim по поводу правомерности использования термина "extraction" закрыт в его пользу.

Отец кок-экстрактора Pierre "какой-то студент" Letouzey употребляет этот термин вольно через предложение в статье по ссылке. Также на эту работу ссылаются пейперы по F* и так же вольно употребляют extraction.

В-общем, на то что extraction это превращение прувов в программы - можно забить. Все всё равно превращают только программы в программы, а CHI-экстракция остаётся не более чем любопытным курьёзом.

В-общем, новое определение экстракшена - это компиляция программ, сохраняющая их свойства (например теоремы доказанные для входного кода остаются верными и для выходного). Под это не подходят только компиляторы, не полностью сохраняющие семантику (например трасляция индуктивного Nat в машинный инт).
СсылкаОставить комментарий

Новости хакатона [мар. 24, 2017|23:27 pm]
Andy Melnikov
[Tags|, ]

Создал тучу тасок по окзору: https://github.com/ptol/oczor/issues/10

В-основном это что-то типа линта, можно все скопом одним коммитом/PR лепить. Ну и делать аналогичное в других файлах, благо там конь не валялся. Главное не переусердствовать. Линейный композиционный стиль - ок, но как начинаются выкрутасы лучше остановиться.

По HNC посрывали низковисящие фрукты, но осталось ещё немного.
СсылкаОставить комментарий

Функциональный календарь [мар. 24, 2017|15:41 pm]
Andy Melnikov
[Tags|]

Как и ожидалось, флаеры разобрали на сувениры, чисто как камни с Парфенона или пирамид.

В следующий раз надо будет сделать календарь с 12-ю ображенными функциональными программистами.
Ссылка1 комментарий|Оставить комментарий

Наше кино [мар. 24, 2017|14:27 pm]
Andy Melnikov
[Tags|]

http://www.imdb.com/title/tt4263270/

Я тут периодически из мазохистских соображений хожу в кинотеатр за компанию. В результате посмотрел две сказки и кучу экшенов, и вчера чуть не попали на Аленький цветочек. Но по доминиканскому традиционному рандому (жизнь здесь крайне непредсказуема) вместо этого пошли на Reinbou.

Оказалось довольно качественное кино. Доминиканцы ржали с правдивости показанного быта в баррио, но потом заскучали, я наслаждался драмой. Это не "драма-драма", но не похожа на мейнстримное латиноамериканское кино. Зрителей вместо было 5 человек не считая троих "нас", что меньше обычного (обычно тоже малая заполненность зала).
СсылкаОставить комментарий

Все со студией и табами! [мар. 22, 2017|18:38 pm]
Andy Melnikov
[Tags|, ]

http://stackoverflow.com/insights/survey/2017/

Опрос показал существование альтернативной реальности, где люди сидят в Студии и делают отступы табами.
Ссылка12 комментариев|Оставить комментарий

navigation
[ viewing | most recent entries ]
[ go | earlier ]