Идеи и инсайты

Исследуем AI-first разработку, кодовые ограждения и архитектуру одноразовости.

LLM могут генерировать код на Rust. Формальные доказательства — это совершенно другая проблема.

Большие языковые модели пишут удивительно хороший код на Rust, но когда вы просите их о формальном доказательстве, они галлюцинируют инварианты и изобретают синтаксис, который не принимает ни один верификатор. Вот что они на самом деле делают правильно, где ломаются и как их всё равно использовать.

LLM могут писать Rust, который компилируется и даже проходит . Что они не могут делать надёжно — так это писать формальное доказательство того, что код…

8 июля 2026 г.

model-checking race-conditions concurrency testing

Ожидание race conditions — ужасная стратегия тестирования

Почему model checking превосходит дни продакшен-рантайма в поиске concurrency-багов и как применить его к собственному коду.

Ждать, пока race conditions проявятся в продакшене, — это не тестирование. Это надежда, замаскированная под добросовестность. Вы можете запускать приложение…

7 июля 2026 г.

model-checking temporal-logic formal-methods verification

Можно верифицировать код с помощью model checking, не изучая temporal logic

Bounded model checkers вроде Kani и реляционные model finders вроде Alloy позволяют проверять свойства с помощью обычных assertions и constraints. Вы жертвуете доказательствами liveness ради кривой обучения, измеряемой часами, а не неделями.

Не нужно изучать линейную темпоральную логику, чтобы использовать model checker. Инструменты вроде Kani, CBMC и Alloy позволяют проверять свойства с помощью…

6 июля 2026 г.

model-checking rust verification formal-methods

Можно доказать корректность кода на Rust, не написав ни одного доказательства, но пространство состояний — это плата

Инструменты model checking вроде Kani позволяют верифицировать свойства Rust с помощью assertions вместо формальных доказательств. Проблема в том, что происходит, когда ваши циклы не имеют маленьких границ.

Можно доказать корректность кода на Rust, не написав ни одного доказательства. Инструмент, который это делает, называется model checker, а для Rust наиболее…

5 июля 2026 г.

model-checking distributed-systems tlaplus protocol-design

Распределённый протокол нельзя покрыть юнит-тестами, но можно проверить модельно

Исправление распределённых багов после деплоя обходится дорого. Модельная проверка позволяет найти их до написания хотя бы одной строчки кода реализации. Вот как это сделать с помощью TLA+.

Распределённый протокол нельзя покрыть юнит-тестами. Юнит-тест запускает один процесс на одной машине в одном порядке. Ваш протокол запускает десять процессов…

4 июля 2026 г.

dsls-bounded-context infrastructure config-management devops

Копирование файлов `.env` между окружениями — это не стратегия конфигурации

Как команды инфраструктуры управляют конфигурацией в dev, staging и production с помощью DSL на контекст, которые делают различия между окружениями явными и типобезопасными.

Ваше окружение staging работает. Ваше окружение production — нет. Разница между их файлами составляет 400 строк, и половина из них — комментарии, которым…

3 июля 2026 г.

dsls-bounded-context llm constrained-generation grammar

Grammar-constrained decoding: заставляем LLMs выдавать валидный синтаксис на каждом токене

LLMs галлюцинируют синтаксис, потому что делают probabilistic sampling токенов. Grammar-constrained decoding фильтрует vocabulary на каждом шаге, так что эмитируются только те токены, которые сохраняют синтаксическую валидность.

Попросите LLM сгенерировать JSON-объект, и рано или поздно он выдаст trailing comma, неэкранированный перевод строки внутри string, или bare word там, где…

2 июля 2026 г.

dsls-bounded-context design-systems llm themes

Перевод с английского на тему — просто. Сделать его детерминированным — вот настоящая проблема.

Можно генерировать дизайн-токены из простых английских описаний, но только если рассматривать описание как DSL с ограниченным контекстом, со схемой-контрактом и снапшот-тестами.

Да, вы можете описать тему на английском и получить работающую дизайн-систему. Подвох в том, что описание на английском — это не промпт. Это исходный файл. И…

1 июля 2026 г.

dsls-bounded-context dsl parser-combinators typescript

Выбрось файл грамматики: пиши свой DSL-парсер на простом TypeScript

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

Если ты когда-либо открывал файл грамматики Yacc и задавался вопросом, почему для создания языка нужно учить второй язык, ты не одинок. Генераторы парсеров…

30 июня 2026 г.

dsls-bounded-context config-validation typescript schemas

Ошибки конфигурации в рантайме — это отказы в продакшене, которые вы согласились допустить

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

Ваше приложение выбрасывает через три часа после начала пятничного вечера. Stack trace указывает на глубоко вложенное свойство объекта конфигурации. Значение —…

29 июня 2026 г.