Jane Street після 25 років скепсису створює команду формальних методів

Упродовж чверті століття позиція Jane Street щодо формальних методів була простою: не цікавить. У новому дописі на блозі торгової фірми ця позиція змінилася. «Останні 25 років я казав людям, що Jane Street як організація просто не цікавиться формальними методами, — пише автор. — Більше так не кажу».

Чому скепсис був виправданим

Допис наголошує: стара позиція не була очевидно хибною. Jane Street активно використовує інструменти для підвищення якості коду, а системи типів — це полегшена форма формальних методів, з якої фірма отримала величезну користь. Проте повна верифікація несла витрати, які рідко виправдовували себе поза окремими випадками, як-от синтез апаратури. Канонічний приклад — seL4, формально верифіковане мікроядро й справжнє досягнення: перевірка 8 700 рядків C зайняла близько 25 людино-років, а кожен рядок вимагав приблизно 23 рядків доведення й пів людино-дня роботи.

Такий компроміс може бути виправданим для критичного з погляду безпеки мікроядра, але не для більшості програмного забезпечення — на думку фірми, навіть не для її найкритичніших систем. А потім з'явилося агентне кодування.

Що змінило агентне кодування

Спершу змінився бік витрат: моделі не здатні самостійно будувати довільно складні доведення, зазначає автор, але вони автоматизують велику частину рутини й дають ці інструменти значно більшій кількості людей, що змінює стару арифметику.

Змінився і бік вигод. Моделі добре влучають у поставлену мету, але гірше підтримують здоров'я кодової бази, і результат тяжіє до «слопу»: надмірно ускладнений, повний дивних помилок і крайніх випадків, часто порушує інваріанти, від яких залежить решта коду. Через це вузьке місце верифікації дорожче, ніж будь-коли, а доведення — сильна форма зворотного зв'язку, потрібного агентам і в навчанні з підкріпленням, і в щоденному кодуванні.

Тести залишаються цінними — Jane Street посилається на тестування на основі властивостей і фазинг — але не покривають весь простір станів. Системи типів натомість дають універсальні гарантії: система, що унеможливлює гонки даних, прибирає їх усі, а типи, які роблять міжсайтовий скриптинг неможливим, роблять це категорично. Лазівки на кшталт Obj.magic існують, але їх можна відстежувати й забороняти.

Чому власна команда

Jane Street твердить, що має незвично вигідну позицію: їй належить OxCaml, власний варіант OCaml, що дозволяє пристосовувати мову до технік, орієнтованих на доведення: модульні специфікації всередині системи типів, обмеження на рівні типів щодо володіння та змінності, методи доведення, вбудовані в саму мову. Користувачі хочуть цих можливостей — у дописі зазначено, що вони скаржаться на повільну появу обіцяних типових функцій, а найважче в дослідженнях мов програмування — знайти того, хто застосує нові ідеї в реальній роботі.

Команда планує короткострокові покращення з негайним ефектом і довгострокові цілі, а також співпрацю з Lean, Dafny, Rocq, Agda та Iris. Jane Street шукає людей до цієї команди в Лондоні та Нью-Йорку.