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