Исследуем AI-first разработку, кодовые ограждения и архитектуру одноразовости.
Bounded model checkers вроде Kani и реляционные model finders вроде Alloy позволяют проверять свойства с помощью обычных assertions и constraints. Вы жертвуете доказательствами liveness ради кривой обучения, измеряемой часами, а не неделями.
Не нужно изучать линейную темпоральную логику, чтобы использовать model checker. Инструменты вроде Kani, CBMC и Alloy позволяют проверять свойства с помощью…
Инструменты model checking вроде Kani позволяют верифицировать свойства Rust с помощью assertions вместо формальных доказательств. Проблема в том, что происходит, когда ваши циклы не имеют маленьких границ.
Можно доказать корректность кода на Rust, не написав ни одного доказательства. Инструмент, который это делает, называется model checker, а для Rust наиболее…
Исправление распределённых багов после деплоя обходится дорого. Модельная проверка позволяет найти их до написания хотя бы одной строчки кода реализации. Вот как это сделать с помощью TLA+.
Распределённый протокол нельзя покрыть юнит-тестами. Юнит-тест запускает один процесс на одной машине в одном порядке. Ваш протокол запускает десять процессов…
Как команды инфраструктуры управляют конфигурацией в dev, staging и production с помощью DSL на контекст, которые делают различия между окружениями явными и типобезопасными.
Ваше окружение staging работает. Ваше окружение production — нет. Разница между их файлами составляет 400 строк, и половина из них — комментарии, которым…
LLMs галлюцинируют синтаксис, потому что делают probabilistic sampling токенов. Grammar-constrained decoding фильтрует vocabulary на каждом шаге, так что эмитируются только те токены, которые сохраняют синтаксическую валидность.
Попросите LLM сгенерировать JSON-объект, и рано или поздно он выдаст trailing comma, неэкранированный перевод строки внутри string, или bare word там, где…
Можно генерировать дизайн-токены из простых английских описаний, но только если рассматривать описание как DSL с ограниченным контекстом, со схемой-контрактом и снапшот-тестами.
Да, вы можете описать тему на английском и получить работающую дизайн-систему. Подвох в том, что описание на английском — это не промпт. Это исходный файл. И…
Генераторы парсеров — избыточны для большинства DSL с ограниченным контекстом. Парсер-комбинаторы позволяют построить рабочий парсер на том же языке, что и приложение, без генерируемого кода и без шагов сборки.
Если ты когда-либо открывал файл грамматики Yacc и задавался вопросом, почему для создания языка нужно учить второй язык, ты не одинок. Генераторы парсеров…
Как отлавливать ошибки конфигурации до того, как приложение начнёт обрабатывать трафик, используя валидацию схем и проверки во время сборки.
Ваше приложение выбрасывает через три часа после начала пятничного вечера. Stack trace указывает на глубоко вложенное свойство объекта конфигурации. Значение —…
Ambient Authority означает, что любой код в вашем процессе Node.js может взаимодействовать с файловой системой, сетью и окружением. Вот как убрать это с помощью lockdown, compartments и явной передачи capabilities.
Одна скомпрометированная транзитивная зависимость может эксфильтровать ваш , записать данные в вашу файловую систему и открыть исходящие соединения. Ей не…
Большая часть доверия между сервисами основана на сетевом расположении, а не на криптографическом доказательстве. Вот как возможности, mTLS и SPIFFE позволяют сервисам аутентифицироваться без окружающего полномочия, и почему это сложнее, чем должно быть.
Ваши микросервисы используют общую VPC, поэтому доверяют друг другу. Это доверие — окружающее полномочие: разрешение на вызов сервиса предоставляется не…