Идеи и инсайты · Страница 6

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Ваши зависимости могут читать переменные окружения. JavaScript им позволяет.

Ambient Authority означает, что любой код в вашем процессе Node.js может взаимодействовать с файловой системой, сетью и окружением. Вот как убрать это с помощью lockdown, compartments и явной передачи capabilities.

Близость в сети — это не идентичность: как сервисы аутентифицируются без окружающего полномочия

Большая часть доверия между сервисами основана на сетевом расположении, а не на криптографическом доказательстве. Вот как возможности, mTLS и SPIFFE позволяют сервисам аутентифицироваться без окружающего полномочия, и почему это сложнее, чем должно быть.