Личные заметки Егора Урванова про AI-разработку, инженерное управление и сообщества. Это взгляд и практика одного автора.
Почему любой код агента нельзя проверить на любое правило, какие три способа делают проверку конечной, как граница агрегата из event storming становится постом проверки, как по проверяемости выбрать размер ограниченного контекста и почему первую рамку важно уметь дёшево сдвигать.
Что говорит теорема Райса и почему проверка поведения программы упирается в проблему остановки. Предикат о тексте и о поведении, доказательство на примере с оплатой, связь с парадоксом брадобрея и три рамки, которые делают проверку точной.
Как посчитать правила игры честно и быстро и могут ли два ответа разойтись. Разбор статьи Бартольди, Бридсона, Михайлова и Николсона о разрыве соотношений (arXiv 2610.23637): игра из двух ходов, где игроку нужны два правила, а бухгалтеру одна запись, со схемами, формулами и выкладками.
Vitest или Jest: настройка, место запуска, стиль проверок. Когда брать Vitest на Vite, оставить Jest или хватит QUnit в браузере. Таблица и вопросы.
Как найти состояние гонки в коде: модель на Quint перебирает порядки действий и показывает цепочку, где правило ломается. Примеры и пределы метода.
Тест проверяет придуманный сценарий, model checking перебирает все порядки действий. Что ловят QUnit, Jest, Vitest и что Quint, TLA+, Alloy. Как выбрать.