Даже формально верифицированный компилятор может ошибаться

В 2011 году исследователи тестировали CompCert случайно сгенерированными C-программами и нашли wrong-code баг в таком выражении:

return -1 <= (1 && x);

Правильный результат — 1, но CompCert 1.6 для PowerPC возвращал 0.

Ошибка оказалась не в доказанно корректном оптимизаторе, а в неверифицированном фронтенде.

Формальная верификация защищает только те части системы, для которых действительно построено доказательство.

Это один из самых изобретательных проектов, которые я видел на этой неделе.

Передаёт файлы между двумя устройствами, используя только экран и камеру. Использует Fountain Codes (LT Codes).

Вместо разделения файла на последовательные фрагменты, каждый QR-код содержит математическую комбинацию (XOR) блоков файла.

Разработчик достиг скорости до 129 КБ/с. Всё работает в браузере с WebAssembly, без установки каких-либо приложений.

https://github.com/bashalarmistalt/decimen-optical-transfer

Сколько незаконченных Git-репозиториев лежит у вас на диске?

drydock показывает их все в одном терминальном интерфейсе:

- где остались незакоммиченные изменения;
- какие коммиты ещё не отправлены;
- где забыты stash, конфликт или незавершённый rebase;
- какие проекты изменились после последнего тега и готовы к новому релизу.

Инструмент проверяет не только текущую ветку, поэтому забытая работа в локальной feature-ветке тоже попадёт в список.

brew install yetidevworks/drydock/drydock

# или
cargo install drydock

После установки достаточно запустить:

drydock

Есть фильтры, fuzzy-поиск, JSON-вывод, открытие проекта в редакторе и массовый fetch. Состояние репозиториев обновляется автоматически через файловый watcher.

drydock написан на Rust с использованием Ratatui и работает на macOS и Linux.

Полезная утилита для разработчиков, у которых папка Projects давно превратилась в кладбище почти законченных идей.

GitHub:
https://github.com/yetidevworks/drydock

Rust, который наконец становится понятным 🦀

Давно хочешь выучить Rust, но ownership, borrowing и lifetimes выглядят как отдельный вид боли?

Этот курс проведёт тебя с самого начала до уровня, где ты уже пишешь реальные системные и сетевые программы.

Ты разберёшь:
Ownership → Borrowing → ошибки → коллекции → Generics → Traits → модули → тесты → сетевой код

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

🔥 Rust с нуля
🔥 5–6 часов в неделю
🔥 Практика после каждого урока
🔥 Подойдёт после Python, JavaScript, Java и других языков
🔥 Можно начать сразу

В конце у тебя будет понимание Rust, с которым уже можно писать быстрые backend-сервисы, сетевые приложения и системные утилиты, а не смотреть на borrow checker как на врага.

Пора добавить Rust в свой стек. Начинай курс и пиши первый код уже сегодня: https://stepik.org/a/294885/

🔥 piqc показывает, сколько денег Kubernetes-кластер теряет на простаивающих GPU

Команды часто видят загрузку GPU, но не понимают:

- какая модель работает на конкретном ускорителе;
- сколько стоит генерация токенов;
- где простаивает железо;
- почему растёт инфраструктурный счёт.

piqc сканирует Kubernetes-кластер и автоматически находит inference-нагрузки на vLLM и Ray Serve.

Инструмент связывает между собой модели, GPU, реплики и runtime-метрики, а затем формирует отчёт о расходах и неэффективном использовании ресурсов.

Что умеет находить piqc:

- простаивающие GPU;
- модели на слишком дорогих ускорителях;
- полностью свободные GPU-узлы;
- фрагментацию ресурсов;
- зависшие в очереди поды;
- низкую эффективность вычислений;
- завышенную стоимость генерации токенов.

Для vLLM также собираются:

- latency;
- скорость prefill и генерации;
- загрузка KV-cache;
- глубина очереди;
- состояние inference-сервиса.

Быстрый запуск:

pipx install piqc
piqc scan --format table

Результаты можно получить в форматах table, JSON, YAML или в виде стандартизированного facts bundle.

Инструмент также запускается внутри кластера как Kubernetes Job - без постоянных агентов и sidecar-контейнеров.

Важная деталь: сейчас проект распространяется по Business Source License 1.1. Переход на Apache 2.0 запланирован на 2028 год.

По сути, piqc отвечает на вопрос, который обычный мониторинг часто оставляет без ответа:

какая именно модель сжигает GPU-бюджет и почему?

GitHub:
https://github.com/paralleliq/piqc

Лето, ИТ-Пикник и музыка известных артистов уже через несколько дней!

8 августа в Коломенском пройдет ИТ-Пикник.

В программе — выступления проекта LAB Антона Беляева, IOWA, Cream Soda, Pompeya, мартина и Совы.

А днем — научпоп-лекции, дискуссии об ИИ и больших языковых моделях, мастер-классы и интерактивы. Полезные знакомства и развлечения тоже будут.

Зарегистрироваться и узнать подробности можно на сайте мероприятия.

В билет входит +1 — можно позвать близких и друзей.

До встречи в месте притяжения ИТ.

Задача, которую фон Нейман решил «слишком гениально»

Два велосипедиста находятся в 30 милях друг от друга и едут навстречу со скоростью 15 миль в час каждый.

Между ними постоянно летает муха со скоростью 30 миль в час, разворачиваясь у каждого велосипедиста. Сколько всего она пролетит до их встречи?

На первый взгляд хочется считать бесконечную последовательность всё более коротких перелётов.

Но решение проще.

Суммарная скорость сближения велосипедистов:

15 + 15 = 30 миль в час

Значит, расстояние в 30 миль они преодолеют за один час.

Муха летает всё это время со скоростью 30 миль в час:

30 × 1 = 30 миль

Ответ: 30 миль.

С этой задачей связывают известную историю о математике Джоне фон Неймане.

Когда он мгновенно назвал правильный ответ, собеседник заметил:

> Большинство пытается складывать бесконечный ряд, хотя достаточно вычислить время встречи.

Фон Нейман якобы ответил:

> А я именно сложил бесконечный ряд.

Хорошее напоминание: гениальный человек не всегда выбирает самый простой путь. Иногда он просто проходит сложный невероятно быстро.

Redis не доверяет обычным строкам C - и вот почему

В C строка заканчивается нулевым байтом \0. Из-за этого strlen() каждый раз проходит весь буфер, а хранить произвольные бинарные данные становится неудобно.

Поэтому Redis использует собственную структуру SDS — Simple Dynamic Strings.

В памяти она выглядит примерно так:

[len][alloc][flags][данные...\0]
                   ↑
                  sds

Перед самими данными Redis хранит метаданные:

- len — текущую длину;
- alloc — размер выделенной памяти;
- flags — тип заголовка.

Благодаря этому длина строки определяется за O(1), а свободное место известно заранее. При добавлении данных Redis не обязан каждый раз заново вычислять размер и перевыделять память.

SDS также остаётся совместимой со многими функциями C: указатель ведёт прямо на буфер, а в конце всё равно находится \0.

Но Redis не зависит от этого терминатора — длина хранится отдельно. Поэтому внутри строки могут находиться нулевые байты, изображения, сериализованные объекты и другие бинарные данные.

Важный нюанс: структура sdshdr из старых примеров сегодня упрощена. Современный Redis выбирает компактный заголовок sdshdr5, sdshdr8, sdshdr16, sdshdr32 или sdshdr64 в зависимости от размера строки.

Небольшой заголовок перед буфером решил сразу три проблемы: быстрое получение длины, безопасную работу с бинарными данными и эффективное расширение строк.

Источник:
https://redis.io/docs/latest/operate/oss_and_stack/reference/internals/internals-sds/
https://github.com/redis/redis/blob/unstable/src/sds.h