иероглифы

бестемы бездаты

…и это ещё nivanych не имеет отношения к деньгам. CTO, видите ли.
http://nicka-startcev.livejournal.com/2975891.html
http://nicka-startcev.livejournal.com/2976243.html
Рашкован типичный ищет, где светло, а не где потерял.
Николай Иваныч — культурный, спокойный человек, учоный нах. А Миша, управляющий, не настолько культурен, хотя и вполне эффективен. Может и нахуй послать, и в ёбыч прописать. Ну или Валеру бы позаёбывать, который собственно платит деньги — реального босса, владельца бизнеса.
Но, конечно, публично опускать Иваныча легче и приятнее. Тем более, у него есть жж-аккаунт, в отличие от других упомянутых (чью манеру ведения дел я не одобряю, но это совершенно не относится к теме поста).
иероглифы

coq + imperative algorithm proving

Делаю вот одну шнягу на окамле. Там есть файл, в нём "блоки данных", состоящие из подблоков малой длины.
И подумал я, что дёргать каждый раз Unix.read (обёртку над read()) не очень гуманно в плане количества вызовов ОС, например.
И решил я реализовать более умный алгоритм чтения-кеширования, читающий в блок размера "дисковый блок * 2", по выравненным смещениям, стараясь читать по границе блока, чтобы не читать ненужные блоки. Однако, кое-где явно нет нужды пропускать данные через буфер, когда ясно, что "цельные блоки" можно прочитать напрямую в строку-получателя.
Но оказалось, что я не смог отладить этот сугубо императивный алгоритм руками, и у меня вообще не было уверенности в том, что он работает правильно. Эти гадские смещения, длины! Невозможно интуитивно проверить, правильно ли сделал. Очень БЕСЕД, знаете ли.

Тогда я взял Coq.
Collapse )

постгрес, хранимые процедуры

Наткнулся на говно. Имею в постгресе хранимку вида
declare
  l_bool boolean;
begin
  l_bool := somefunc();
  return query select * from
    (select * from table where l_bool
     union all
     select * from table where not l_bool and ...
    );

И вот, при замене в запросе переменной l_bool на литерал с реальным значением я получаю 5мс вместо 1600мс.
Это -- не то "кеширование планов", которое хорошо задокументировано в мануле, это что-то другое, так как "кеширование планов" работает при первом вызове функции в пределах сессии, а я вызываю эту функцию с одним и тем же параметром как до, так и после изменения. И это не затраты на парсинг + построение планов, так как последующие запуски показывают примерно то же время.
А план запроса "с переменными" не посмотреть, так как explain хочет на входе полноценный, умеющий выполняться запрос.
В оракле такой хуйни не было!

построение термов тактиками в coq -- безопасно

Сегодня thedeemon показал ужосы, от которых у меня волосы в жилах стынут.
А мне стало интересно, можно ли накосячить подобным образом в coq.
Но писал я быстро, поэтому код некрасивый. Например, можно спокойно попрятать многое в implicit arguments, да и для vec выбрать более кошерный тип (например, кошерный в плане strict positivity).

Collapse )

Однако, кое-какая лажа у меня таки была. Если rewrite, ныне вынесенный в vec_cast, натравить не на чистый пруф-терм ("n = m -> length l = n -> length l = m"), а на computational term (в том числе содержащий пруф) ("n = m -> vec A n -> vec A m"), то Eval compute выдаёт совершенно аццкий терм, содержащий в том числе пруф того, что длины равны. Но в #coq быстро объяснили, в чём дело. В этом состоит мой личный профит от этой задачки. Ну и развлёкся, и убедился, что в coq подобные косяки допустить трудно, даже если используются тактики.

Опыт использования Coq на практике, или Как я сам себя отпетушил COQОКОКОКО

Есть время собирать опыт.

Есть время разбрасывать на вентилятор.




Уже довольно давно система типизации в окамле кажется мне слегка недостаточной.
Collapse )

По итогу -- впечатления смешанные.

coq + inlining + "merge right"

Некоторые люди прочитали статью http://alaska-kamtchatka.blogspot.com/2012/08/merge-right.html , где была показана весьма общая функция для слияния/пересечения/разницы списков.
А господин ygrek в камлочятике прилюдно мучил MetaOCaml для инлайнинга функций-аргументов merge. Я не мог на это смотреть спокойно. Однако и сразу разобраться не смог, так как не знал многого, но вполне так узнал.
Чтобы было хоть сколько-нибудь интересно читать, рекомендую прочитать сначала исходную статью.
Потому что сейчас будет простыня.
Collapse )
Вроде ЗБС.
Можно было бы сравнение не инлайнить, но избавиться от вызова функции (будь то "(fun (a : int) b -> ...)", будь то Pervasives.compare) не получается сходу.
Мне Coq нужен не только для зависимых типов и доказательств кода, но и для инлайнинга. Я -- практичная скотина, да!
Если будут вопросы -- поясню. Потому что всё сразу пояснять -- руки устанут.

год

Интересно просуммировать, что же я сделал за год. (дата выбрана совершенно случайно, но "новый год" выбирать как-то неоригинально.) Не упорядочено никак. И не пишу, благодаря кому это делал -- слишком многих перечислять придётся.
Collapse )

upd1/
Collapse )

upd2/
Collapse )

upd3/
Collapse )

вся правда про меня

Я считаю, что люди, читающие мою жыжыцу, должны знать всю правду про меня.
Автора данного текста я не называю, и вы не называйте, даже если знаете. Тем более, вытащено из подзамочного поста, что, в принципе, не очень хорошо. И каменты на всякий случай буду скринить. Да и не в авторе суть, а в тексте.
Просто учтите, что я вот такое вот говно.

Не тебе судить.
Да, для работы с ленивостью в реальных больших проектах, где условно говоря, много "IO", нужен некоторый опыт. А примеры твои ничего не стоят.
Остальное, в GHC/Haskell, ты откидываешь. И уже вполне приблизился к фанатизму "раз этого нет в любимом инструменте, то это не нужно".
Твои познания за использование ленивости только очень теоретические. Причём, специфической направленности — выискиывать различные fuckup'ы с ленивостью. Вот я тебя спрошу — а приведи примеров хороших и грамотных решений? Ты нормально не ответишь. Зато примеры fuckup'ов привести сможешь.
Ты не разбираешься в теме. Не тебе судить.