В связи с наличием языка F# и недавним появлением языка F*, предрекаю появление языка, объединяющего F#, F* и новый, пока не созданный F$, и название у него будет F#*$.

#oezzhg

9 comments

Фраза "удалённая работа" имеет два смысла, и переводы на английский таковы: "remote work" и "removed work". Интересно, созвучность этих слов в английском языке является простым совпадением, или она чем-то обоснована?

#osnneg

add comment

Конечно, читать и пеарить этого _жжюзера_ (в худшем смысле этого слова) как бы моветон, но я его и не читаю на регулярной основе, мне ссылку скинули, а пеарить конкретный пост можно хотя бы потому, что он содержит краткое русскоязычное описание "помидорок" — такой специальной полезной техники, которая позволяет ... more →

#osnnes

10 comments

В периоды жизни, когда у меня липкое говно, я сливаю немного воды в унитаз, и на эту воду "приклеиваю" туалетную бумагу к унитазу (обычно достаточно сложить бумагу в форме заглавной буквы "лямбда"). Когда наступает счастливый момент калоизвержения, говно роняется на бумагу, а не на унитаз, и всё это миленько так ... more →

#osngzg

11 comments

сейчас наткнулся на подобную штуку, и немного генерализирую.
при написании веб-сервера на coq обнаружим, что рекурсивная функция, читающая http-заголовки, внезапно потребует доказательства завершимости. По идее, оно должно включить в себя конечность числа символов в прочитанных заголовках, либо конечность как числа ... more →

#osgisi

add comment

за пару дней научился: 1. вгонять одномесячного дитя в сон с >половинной вероятностью, 2. менять памперсы, 3. лежать дитя "на руках" без нытья, если в неэкстремальных случаях.
Я крут.
Ну, всякие там прогулки по городу с коляской не считаются, это же для любого мужика прикольно, машинки и всё такое.

#osgtgt

7 comments

I heard Coq like types, so we put type in your type so you can type your types while you are typing your types.

и больше ничего не могу сказать про текущие дела :)

#osgtte

7 comments

к моему посту #osofnz — Олег Киселёв пишет в caml-list:
"Somehow typed tagless interpreters (embeddings of a typed language) and length-parameterized lists with the append function are the most popular examples of GADTs. Neither of them seem to be particularly good or compelling examples. One can write typed ... more →

#osehhh

2 comments

днём температура поднялась до +23, пиздец просто. В рубашке ходить, штоле. Уже включаю кондиционер дома. Весна, блеять.
Но у нас такая весна всегда: то +10 подержится недельку, потом +15, а потом уже +25 и выше, и хорошо, если +30 не будет достигнуто за месяц.
Вот такая хуёвая весна.

#osstot

9 comments

есть "репперы", которые, в целом, поют (или "читают"?) об этом же говне, но настолько виртуозно владеют русским языком, что мне нравится. Плюс к тому, стёб над реппом в громадных количествах. Только две "группы" умеют виртуозно: 1. "кровосток" (лучше брать сразу полное собрание сочинений), 2. "дядя женя" (проще ... more →

#osionn

14 comments

ааа, убейте меня, иначе я всё забрызгаю тут1111
@default631">http://flint.cs.yale.edu/cs428/coq/doc/R...
СУТЬ:
У вас есть индуктивный тип данных для представления вашего игрушечного AST, специфичного для вашей предметной области.
У вас есть функция, преобразующая _ваши_ значения из AST в ... more →

#osfnnt

6 comments

Вышла курочка считать
Маленьких цыпляток.
Белых пять и серых пять,
А всего — ... МАМА ТЫ ЧО ВАЩЕ В КОНЕЦ ОХУЕЛА МНЕ ПОЛТОРА ГОДА МЫ ТАКОЕ В САДИКЕ НЕ ПРОХОДИЛИ КАКАЯ В ЖОПУ ДЕСЯТИЧНАЯ СИСТЕМА СЧИСЛЕНИЯ КАКИЕ В ЖОПУ ЦЫПЛЯТА НУ ВООБЩЕ ПИЗДЕЦ

#osffih

add comment

http://pit.dirty.ru/lepro/2/2012/03/14/5...

#osfheg

10 comments

true <> false
Неожиданно? Однако, это так.
Эта шокирующая истина теперь конструктивно доказана: http://gds.livejournal.com/63887.html

#osheot

2 comments

http://gds.livejournal.com/63527.html — как обычно, интересуют каменты там либо тут. (не нравится щёлкать на ссылку — не щёлкайте, но копипастить ту простыню сюда я не буду.)

#oshhoh

add comment

не прошло и двух недель, как индеец Зоркий Глаз обнаружил галочку "Allow access for authenticated users only" и понял, почему всякие 403 бывают, когда кому-то даёшь ссылоту на чужое псто.

#oshzzi

6 comments

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

#ostnnh

13 comments

прямо с утра накатил шампанского, заел бутером с красной икрой, наварил кофе, покормил кошаков мясом, раскурил вчерашнюю трубку.
хотел бы извиниться за попытку общения с одной хорошей леди, которая меня читает тут, но до собственно общения не дошло. (однако, на новом ноуте наладил скайпик, там даже вебкамера есть, ... more →

#ostsnf

2 comments

блядь, какого-то хуя посрался с депутатшей верховного совета страны. в рамках дискуссии предложил ей "уебать с ноги по гнусному ебалу". мне пиздец, пасаны :]]

#ostito

5 comments

посоны, посоветуйте, куда обращаться / по каким словам гуглить.
в /usr/share/X11/locale/$LANG/Compose находится только include файла, который содержит, в том числе, строку:
<Multi_key> <equal> <greater> : "⇒" U21D2 # RIGHT DOUBLE ARROW
однако, данная комбинация не работает, в отличие от других, описанных ... more →

#osthsg

add comment

Вы — читатель псача, но не знаете, сколько времени держать кофе на огне?
Тогда для вас есть хорошее мнемоническое правило:
ШАПКА ВСТАНЕТ — КОФЕ РАЗЛИВАТЬ БУДЕМ

#osthhh

6 comments

Придумал годный психологический тест. А интерпретацию ответов придумайте сами, не маленькие.

Если нельзя, но очень хочется, то ...
— можно
— нельзя
— можно, только осторожно
— не так уж и хочется
— можно, но не нужно
— нужно, но негде

#osoiih

23 comments

http://dou.ua/lenta/articles/chtoby-razr...

#osoiho

3 comments

интересно, "подъ'ерж'иваю" — это то же самое, что "поджидаю"?

#osoite

add comment

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

#osofnz

7 comments