(no subject)

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

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

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

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


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

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

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

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

(no subject)

Решил вынести ответ на камент в отдельный пост. Так как дело было в жыжыцэ, пост будет тоже жэжэшный.

Исходный комментарий -- http://diam-2003.livejournal.com/527676.html?thread=1267516#t1267516 :
> Но ведь с другой стороны, у людей, которые всё это пишут, тоже ведь есть мозг.

Конечно есть, но мотивы их писюлек далеко не всегда исходят из желания "сделать людям хорошо", и не из желания поделиться _работающим_ решением (особенно учитывая, что про подобные решения, работающие на практике, мало кто слышал -- а какая-то информация таки просочилась бы).
Collapse )

Теория такая теория.

coq, reversed lists

Взял несложную (как казалось) задачку, потыкал в неё палочкой, отчаялся, дошёл до #coq irc, изложил проблему, но не помогли. Зато теперь есть изложение этой проблемы:
Collapse )

Может, у вас будут идеи?

UPD/
Подсказали. Definition my_list_rev_mapped := Eval compute in предыдущее_определение. И всё, что оно может, оно вычисляет в compile time. Как же мне это нравится!

coq, zgtz

Решил вспомнить молодость и подоказывать кое-что. У известного Адама взял какой-то пример, который он доказывает через свою придуманную для книги CPDT тактику "crush", но мне это не нравится. Хотя бы тем, что тактики не нравятся. Я хочу что-то более приближённое к конструктивному построению доказательства.
Итак, "ноль не больше нуля" с моим тупым доказательством через классические тактики.
Lemma zgtz : 0 > 0 -> False.
intro H. inversion H.
Qed.
Print zgtz.

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

dependent types

(как бы разворачивая каменты из предыдущего поста)

А расскажите, где вообще полезны dependent types?
Про примеры с массивами и их границами я в курсе, но это мало полезно лично мне на практике -- дело в том, что я как-то не нарывался на проблемы с этим уже несколько лет, причём dependent types не использовал для этого никак, ни разу. (а вот модульность и нормальные интерфейсы модулей -- как раз использовал.)
Далее, понятно, с помощью dependent types можно протаскивать какие-то утверждения в compile time. Очень хорошо, но с какими практическими целями?
Что я уже читал: первые несколько страниц выдачи гугла по "dependent types", в том числе известное "why dependent types matter". И, всё равно, либо dependent types это малонужная хуйня, либо я тупой. (не стесняйтесь, я прекрасно знаю свои интеллектуальные способности, поэтому последний вариант не оскорбителен.)

blog + jabber

Одна из частей моего интернет-общения с людьми состоит в том, что я шлю одинаковые/похожие сообщения по жабберу нескольким людям одновременно.
По идее, для автоматизации этого процесса нужен блог/микроблог (тьфуты, пойду помою язык) с поддержкой возможности постить через жаббер и с возможностью людей "подписаться" (так, чтобы им в жаббер приходили мои "посты").
Вот его и попытаюсь найти, а вы, читающие этот пост, может быть подскажете, что мне подойдёт. Вдруг сталкивались или слышали о подобном.
Сразу скажу, что твитор и жуйк мне не подходят, по разным, но весьма серьёзным причинам, их давайте откинем, даже если они удовлетворяют описанным мной требованиям.
От подобного сервиса очень желательно иметь возможность видеть в вебморде эти "посты", хотя бы чтобы можно было на них сослаться http-ссылкой, ну и для любителей эфпячить вместо более культурных средств. Ещё очень хочется rss/atom и подобное, для тех, кто предпочитает не реалтайм-доставку жаббером, а чтение фидов.
Это -- минимальные требования к сервису. Больше и не нужно. Всякие каменты -- хрен его знает, нужны ли. Будут -- хорошо, не будут -- проживу.
Подскажите, есть ли в интернетах бесплатный сервис, предоставляющий подобную функциональность?

rdbms, global id / hosts

А теперь -- о тупой практике вопрос.
Задаю тут, так как знаю, что по крайней мере четверо из читающих меня людей сталкивались с этой проблемой.
Хочется в пределах реляционной базы данных сделать так, чтобы id записей с разных, но подконтрольных мне баз данных не перекрывали друг друга, и при этом могли генерироваться независимо и локально.
Конечная цель -- создавать такие строки таблиц, чтобы таблицы можно было сливать-разливать по необходимости.
Я знаю только два хака для этого.
1. Прямой хак: сделать так, чтобы первичный ключ записи включал в себя (local_id serial, host_id integer) (вариант -- host_name varchar). Хорошо тем, что индекс по (local_id, host_id) в большинстве случаев (для запросов по локальным данным) будет ровно настолько же селективен, как и просто по local_id. Хотя он будет жирнее, что не радует. Ещё больше не радует то, что соединять таблицы придётся по двум полям, внешние ключи тоже будут по двум полям.
1а. Вариант прямого хака: иметь local_id, host_id, но формировать из них уникальную строку (например, тупо, "123.456" для local_id=123 и host_id=456, или более умно, побитово), которую уже считать идентификатором. Нормально, но первичные/внешние ключи по строковым типам обычно медленнее, чем по numeric типам. И вообще, какое-то сомнительное решение.
2. Кривой хак: закодировать host_id в самом id, например, выделяя какие-то биты (старшие/младшие) под host_id, остальные биты оставляя под local_id. Не нравится тем, что этим сильно ограничивается либо диапазон host_id, либо диапазон local_id, и это потребует проверки со стороны программы (либо ошибки со стороны бд), попадает ли новый локально-сгенерированный id в то множество host_id, в которое он должен попадать. А мне нужно для постгреса, а там самый большой целочисленный тип хранит 8 байт, и не уверен, что их хватит в случае таблиц, с которыми будет вестись интенсивная работа. Кроме того, решение хуже тем, что где-то нужно централизованно выдавать host_id, тогда как решение из п.1 с host_name требует только разумной выдачи host_name, такой, чтобы они не пересекались.

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

(думал поставить на этот пост "тематику только для взрослых", но уже запечатал конверт.)