Category: техника

Category was added automatically. Read all entries about "техника".

иероглифы

coq + imperative algorithm proving

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

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

(no subject)

ответ на очередное тупопёздничество этой леди, на этот раз тут: http://nicka-startcev.livejournal.com/1651259.html?thread=5538875#t5538875

(кстати, удивлён, что ребе Белнетмон как-то умудрился не хамить открыто.)

> когда меня манагер спрашивает, сколько времени займёт разработка такого-то девайса, я всегда говорю: столько, сколько нужно, плюс время, которое мы тратим сейчас на эту бесполезную болтовню :)

Разработка для разработки. Это так мило. Косвенно напоминает известный анекдот про "откуда деньги берутся? из тумбочки.". Ебануться можно. Налицо тупое непонимание того, что результат работы и сроки готовности результата _напрямую_ влияют на прибыль компании. (Или там такая компания, где делай что хочешь, забивай болт по необходимости, но деньги всё равно будут идти? Даже с заранее увеличенными в несколько раз сроками, определяемыми левой пяткой разработчика? Тогда я бы тоже поработал там, если не совсем нищенская зарплата.)


> чем больше разработчику предоставляется благ - тем эффективнее он работает.

Пока не начинает понимать, что можно и не работать, а прокрастинировать, заниматься хуйнёй, чесать лиловую лысину на рабочем месте, драться саблями (пруф в xkcd). До наступления этого понимания проходит не так уж много времени (если разработчик умный), и тогда у организации начинает медленно подниматься вопрос про то, что и как делать дальше с этой вашей разработкой. Просто увольнять невыполняющего работу сотрудника -- гемор, я читал ТК рашки и приднестрашки. И не надо говорить, что все люди пиздец какие честные, и все просто одержимы тупым кодингом всякой хуйни.

> а заполнение бумажек только отнимает время, отвлекает от основной задачи и раздражает, заставляет лишний раз подумать о смене работы

А ещё бывает так, что разработчик долбится рогами в совершенно другие ворота, не в те, в которые нужно. Конечно, если дело не в тупых микроконтроллерах, где всё, что нужно от обезьянки-кодера -- это всосать несложную предметную область и хуярить на какой-нибудь сишечььке.
Кроме того, для лучшего результата, бывает, нужно сверху как-то повлиять -- показать более кошерный способ реализации, переосмыслить ТЗ, чуток поменять архитектуру. А если каждому разработчику дать полную свободу от бумажек (в том числе от тех, где он описывает архитектуру, планы и сроки) -- поимеем и хуёвую архитектуру, и кривые×неактуальные планы, и проёбанные сроки. И, в рот тебе ноги, проёбанную прибыль компании. Хотя, опять же, если дело ремесленное -- будь то настраивать проводки в 1С, будь то писать дейтинги и дорвеи на похапэ, будь то лепить тупой говнокод на микроконтроллерах -- вполне можно дать разработчикам швабодку. Проблемы начнутся попозже, в таком случае.