В Jane Street 25 лет твердили, что формальные методы организации неинтересны. Теперь это не так. Раньше их считали слишком дорогими для большинства проектов. Хрестоматийный пример — seL4: формально верифицированное микроядро. 25 человеко-лет на 8700 строк C, каждая строка кода требовала в среднем 23 строки доказательств и полчеловеко-дня проверки. Для security-критичных вещей — ок, но для обычного софта, даже самого важного, овчинка не стоила выделки.
Появление agentic coding всё перевернуло. Теперь в Jane Street строят команду, которая займётся формальными методами. Надеются сделать их таким же повсеместно полезным инструментом, как сегодняшние сложные системы типов.
Почему передумали? Во-первых, агенты резко снизили порог входа. Модели не умеют сами доказывать сложные теоремы, но они сильно помогают и расширяют круг людей, способных продуктивно использовать формальные методы. Старый расчёт затрат и выгод надо пересматривать.
Во-вторых, выгоды стали выше. Модели здорово пишут код, но он всё больше напоминает slop — переусложнённый, с дикими багами и угловыми случаями, нарушающий инварианты кодовой базы. Людям приходится тратить уйму времени на верификацию такого кода. Формальные методы могли бы снять часть этой нагрузки, сделать ревью эффективнее.
Кроме того, агенты отлично потребляют обратную связь — и при RL-тренировке, и прямо во время написания кода. Формальные методы дают ещё один мощный канал обратной связи, повышая способность агентов решать сложные задачи.
Тесты — круто, но недостаточно. Они не покрывают всё пространство состояний программы. На своём опыте с OxCaml в Jane Street увидели, насколько агентам помогают универсальные гарантии типовых систем. Если типы запрещают data races — их действительно не будет. Если типы делают невозможными XSS-уязвимости — они и не появятся. Тесты так не умеют.
Почему именно Jane Street может этим заняться? У них глубокий контроль над языком OxCaml — можно адаптировать его под доказательные техники. И есть сообщество программистов, готовых к таким штукам: пользователи злятся, если обещанные странные фичи типовой системы не поставляются достаточно быстро. Эта база даёт свободу пробовать и близкие улучшения, и амбициозные долгосрочные планы.
Они вдохновляются работами сообществ вокруг Lean, Dafny, Rocq, Agda, Iris и других. Планируют интегрировать OxCaml с некоторыми из этих инструментов, но хотят получить уникальные преимущества от одновременной работы над языком и техниками доказательств.
Сейчас ищут людей в Лондоне и Нью-Йорке, команда только собирается, работы — непочатый край.