Jane Street 25 yıllık şüpheciliği bırakıp biçimsel yöntemler ekibi kuruyor

Çeyrek yüzyıl boyunca Jane Street'in biçimsel yöntemlere bakışı basitti: ilgilenmiyoruz. Alım satım firmasının blogunda yayımlanan yeni bir yazıda bu tutum değişti. "Son 25 yıldır insanlara Jane Street'in bir kurum olarak biçimsel yöntemlerle ilgilenmediğini söylüyordum" diye yazıyor yazar. "Artık bunu söylemiyorum."

Şüphecilik neden makuldü

Yazı, eski tutumun açıkça yanlış olmadığını özellikle belirtiyor. Jane Street kod kalitesini artıran araçları yoğun biçimde kullanıyor ve tip sistemleri de firmanın büyük fayda sağladığı hafif bir biçimsel yöntem türü. Ancak tam doğrulama, donanım sentezi gibi özel durumların dışında nadiren karşılığını veren maliyetler taşıyordu. Klasik örnek seL4: biçimsel olarak doğrulanmış bir mikro çekirdek ve gerçek bir başarı. 8.700 satır C kodunu doğrulamak yaklaşık 25 kişi-yıl sürdü; her satır için kabaca 23 satır ispat ve yarım kişi-gün gerekti.

Böyle bir denge güvenlik açısından kritik bir mikro çekirdek için mantıklı olabilir, ama çoğu yazılım için — firmanın kendi en kritik sistemleri için bile — anlamlı görünmüyordu. Sonra ajan tabanlı kodlama geldi.

Ajan tabanlı kodlama neyi değiştirdi

Önce maliyet tarafı değişti: modeller tek başlarına son derece zor ispatları kuramıyor, diyor yazar, ama angaryanın büyük bölümünü otomatikleştiriyor ve bu araçları çok daha fazla insanın eline veriyor; bu da eski hesabı değiştiriyor.

Fayda tarafı da değişti. Modeller belirlenen hedefe ulaşmakta iyi, kod tabanının sağlığını korumakta ise zayıf; sonuç "slop"a kayıyor: aşırı karmaşık, tuhaf hatalar ve uç durumlarla dolu, çoğu zaman kod tabanının temel değişmezlerini çiğneyen kod. Bu da doğrulama darboğazını her zamankinden pahalı hale getiriyor; ispatlar ise ajanların hem RL eğitiminde hem günlük kodlamada ihtiyaç duyduğu geri bildirimin güçlü bir biçimi.

Testler değerini koruyor — Jane Street özellik tabanlı testler ile fuzzing'e işaret ediyor — ama tüm durum uzayını kapsayamıyorlar. Tip sistemleri bunun yerine evrensel garantiler veriyor: veri yarışlarını önleyen bir sistem onları tamamen ortadan kaldırıyor; siteler arası betik çalıştırmayı imkânsız kılan tipler bunu kategorik olarak yapıyor. Obj.magic gibi kaçış kapıları var, ama izlenip yasaklanabilir.

Neden kendi bünyesinde

Jane Street bu iş için alışılmadık derecede iyi konumlandığını savunuyor: kendi OCaml sürümü OxCaml'i kontrol ediyor, bu da dili ispata yönelik teknikler için şekillendirmesine izin veriyor: tip sistemine gömülü modüler spesifikasyonlar, sahiplik ve değiştirilebilirlik üzerine tip düzeyinde kısıtlar, dilin içine yerleştirilmiş ispat yöntemleri. Kullanıcı tabanı da bunu istiyor — yazıda kullanıcıların söz verilen tip özelliklerinin yavaş gelmesinden şikâyet ettiği, programlama dilleri araştırmasında en zor kısmın ise fikirleri gerçek işte kullanacak birini bulmak olduğu belirtiliyor.

Ekip, etkisi hemen görülecek kısa vadeli iyileştirmeleri uzun vadeli hedeflerle birleştirmeyi ve Lean, Dafny, Rocq, Agda, Iris gibi araçlarla işbirliğini sürdürmeyi planlıyor. Jane Street bu ekip için Londra ve New York'ta çalışan arıyor.