Интересная статья про доказательство корректности программ, точнее, почему оно редко применяется на практике. TLDR:

• Чтобы что-то доказать, нужны четкие требования и спецификация. Их получить довольно тяжело, если вообще возможно.
• Надо понимать, что хотим получить от верификации. В бизнесе всем насрать, правильно ли у тебя сортировка работает, если клиенты не приносят бабки.
• Надо формализовать хотелки. Человеческие понятия тяжело формализовать. Кстати, эта же проблема — причина многих проблем с безопасностью ИИ.
• Доказывать что то формально — тяжело. Например, доказать ассоциативность сложения — либо дорого, либо опасно (например, в C++ сложение не ассоциативно в районе INT_MAX).
• Чем язык богаче фичами, тем тяжелее в нем доказать что-то.
• В повседневной работе хороших тестов и документации достаточно для приемлемо хорошего качества. Каждый следующий “процент качества” обычно кратно дороже предыдущего.
• Многие проблемы лежат на уровне проектирования. Но в него почти никто не вкладывается, потому что мало кто понимает его ценность. Большой вклад вносит культурный барьер.

Более-менее серьезные пулл-реквесты довольно неудобно смотреть в самом GitHub. Даже переключение diff на две колонки (split-view) не очень помогает: например, лично мне не хватало дерева файлов. Делать ревью через Intellij стало уныло с обновлением интерфейса — там есть просто позорные баги.

Но можно на странице PR нажать обычную точку ., и будет загружена веб-версия VS Сode, в которой делать ревью приятнее. Причем можно ставить плагины (хоть и не все работают полноценно).

def is_prime(n):
    return re.match(r'^1?$|^(11+?)\1+$', '1' * n) is None

Забавный, хоть и не очень оптимальный способ проверки числа на простоту. Сложность большая, т.к. по сути все числа последовательно перебираются, да потом проходится вся строка заново. Регулярка довольно старая, можно найти упоминания еще в 1998.

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

С одной стороны, недавно был релиз, и он еще используется в Mozilla, nginx. Но, например, Facebook планирует отказываться от него.

Даже до прекращения поддержки на BitBucket, Mercurial’ом пользовалось около 3% людей. Доля пользователей Mercurial была мала даже в 2010х. Если посмотреть на тренды гугла или поискать вакансии, то у Mercurial все грустно.

Так что да, Mercurial скорее мертв, чем жив. Немного жаль, ведь команды Mercurial более интуитивны, да и сам он проще и логичнее. Хотя сейчас почти всю работу в этом плане делают среды разработки, которые поддерживают в основном только git, а остальное — по остаточному принципу.

Интересный доклад про производительность и как ее правильно измерять. Доклад из введения и двух частей.

Суть первой части:

• производительность приложения довольно сильно зависит от расположения кода и данных в памяти, разница может доходить до 40%;
• почти любое изменение кода это расположение меняет;
• оно еще зависит от порядка линковки, размера переменных окружения, версий библиотек, текущей директории и т.п.
• чувак разработал инструмент, который рандомизирует расположение и позволяет понять лучше влияние изменений на производительность;
• эксперименты показали, что -O2 и -O3 статистически неразличимы.

Суть второй части:

• большинство профилировщиков подталкивают на оптимизацию узких мест;
• этот подход плохо работает для многопоточных приложений;
• вместо этого надо анализировать DAG вычислений/зависимостей, и искать места, оптимизация которых реально поможет — как будто они лежат на критическом пути в диаграмме Ганта;
• а еще многие профилировщики измеряют время в контексте всей жизни приложения, а не функции (например, выполнения HTTP-запроса), и чувак сделал профилировщик, который позволяет измерять пропускную способность от точки до точки;
• под конец результаты оптимизаций на основе анализа результата профилировщиков.

Коротенькая обучалка, с которой можно немного поиграться. К сожалению, дает лишь горстку новых знаний, даже толком не рассказывает о том, какая разница между A и AAAA, какие вообще бывают типы записей DNS или что в DNS записи можно напихать почти произвольный текст:

dig txt +short maybethiscould.work

Бывает, что нужно выгрузить кусочек данных, чтобы, например, положить проблемную запись с прода в тестовую базу. В PostgreSql для этого есть два способа: COPY и pg_dump.

Но у обоих есть недостатки: COPY может выгрузить данные по запросу, но только в CSV формате. А pg_dump может выгрузить в формате sql-скрипта, но только всю таблицу целиком. Но если таблица не очень гигантская, то поможет grep:

pg_dump --table=table_name --data-only --column-inserts --dbname=postgresql://user:pass@ip:5432/dbname > dump.txt
cat dump.txt | grep some_id

Классный интерпретатор λ-выражений со встроенным обучением λ-исчислению. 42 задания, первые штук 15 — обучение синтаксису, но потом пойдет веселее. Например, в 25-26 задании можно узнать, что такое Y-комбинатор, а в 30 будет первое задание на вычисление чего-нибудь. Под конец можно будет научиться складывать числа (и это тяжелее, чем возведение в степень!).

Бонус для тех, кто дошел до конца:

(λpdri .rdmpl pi et) oY_ (λa . (FALSE ONE t)a)(ZERO dd)s!

Git — очень гибкий инструмент. Хоть по умолчанию его утилиты, такие как diff и merge, работают со всеми файлами как с текстовыми, это можно изменить. Например, можно переопределить драйвер для merge и мержить xml файлы менее болезненно. Или показывать diff для офисных файлов — один из моих студентов так диплом хранит (не приучен к латеху, увы).

Статья-указатель на оные. Вкратце, есть три группы моделей:

1. Централизованные — для решения глобальных проблем и проблем координации: стратегии, стандарты, ценности, постановка целей, метрики и приоритезация.
2. Основанные на конкретной роли — для редких случаев: менеджер глобальных проектов (программ), интегратор, контролер, разработчик стандартов.
3. Для координации команд — самая большая категория, 17 штук.

По сути это паттерны для построения организации, которые можно применять для улучшения текущих процессов.