Jane Street 25 illik şübhədən sonra formal metodlar komandası qurur

Dörddə bir əsr ərzində Jane Street-in formal metodlara münasibəti sadə idi: maraqlanmırıq. Ticarət şirkətinin bloqunda dərc olunan yeni yazıda bu mövqe dəyişib. "Son 25 ildir insanlara Jane Street-in bir təşkilat olaraq formal metodlarla maraqlanmadığını deyirdim", — yazır müəllif. — "İndi bunu demirəm."

Şübhə nə üçün əsaslı idi

Yazı xüsusi olaraq qeyd edir ki, köhnə mövqe açıq-aşkar yanlış deyildi. Jane Street kod keyfiyyətini yaxşılaşdıran alətlərdən geniş istifadə edir, tip sistemləri isə şirkətin böyük fayda götürdüyü yüngül formal metod növüdür. Lakin tam verifikasiya xərcləri xüsusi hallar, məsələn aparat sintezi istisna olmaqla, nadir hallarda özünü doğruldurdu. Klassik nümunə seL4-dür: formal olaraq təsdiqlənmiş mikro nüvə və əsl nailiyyət. 8 700 sətir C kodunu təsdiqləmək təxminən 25 nəfər-il çəkdi; hər sətir üçün təqribən 23 sətir sübut və yarım nəfər-gün tələb olunurdu.

Belə balans təhlükəsizlik baxımından kritik mikro nüvə üçün məqbul ola bilər, amma proqram təminatının çoxu üçün — şirkətin öz ən kritik sistemləri üçün belə — məntiqli görünmürdü. Sonra agent əsaslı kodlaşdırma gəldi.

Agent əsaslı kodlaşdırma nəyi dəyişdi

Əvvəlcə xərc tərəfi dəyişdi: modellər təkbaşına son dərəcə çətin sübutlar qura bilmir, qeyd edir müəllif, amma zəhmətli işin böyük hissəsini avtomatlaşdırır və bu alətləri daha çox insanın əlinə verir; bu da köhnə hesabı dəyişir.

Fayda tərəfi də dəyişdi. Modellər qoyulan hədəfə çatmaqda yaxşıdır, kod bazasının sağlamlığını qorumaqda isə zəifdir və nəticə "slop"a meyllidir: həddindən artıq mürəkkəb, qəribə xətalar və kənar hallarla dolu, çox vaxt kod bazasının əsas invariantlarını pozan. Bu da verifikasiya maneəsini hər zamankindən baha edir; sübutlar isə agentlərin həm RL təlimində, həm gündəlik kodlaşdırmada ehtiyac duyduğu əks əlaqənin güclü formasıdır.

Testlər dəyərlidir — Jane Street xassə əsaslı testləri və fuzzinqi göstərir — lakin bütün vəziyyət fəzasını əhatə edə bilmir. Tip sistemləri isə universal təminat verir: məlumat yarışlarını istisna edən sistem onları tamamilə aradan qaldırır, saytlararası skriptləşdirməni qeyri-mümkün edən tiplər bunu kateqorik edir. Obj.magic kimi çıxış yolları var, amma izlənib qadağan edilə bilər.

Nə üçün daxildə qurulur

Jane Street bu iş üçün qeyri-adi dərəcədə yaxşı mövqedə olduğunu iddia edir: OCaml-in öz variantı OxCaml-ə nəzarət edir və bu, dili sübut yönümlü texnikalara uyğunlaşdırmağa imkan verir: tip sisteminə daxil edilmiş modul spesifikasiyaları, sahiblik və dəyişkənlik üzrə tip səviyyəsində məhdudiyyətlər, dilin özünə yerləşdirilmiş sübut üsulları. İstifadəçilər də bunu istəyir: yazıda qeyd olunur ki, onlar vəd edilən tip xüsusiyyətlərinin gecikməsindən şikayət edir, ən çətin hissə isə ideyaları real işdə istifadə edəcək insan tapmaqdır.

Komanda qısamüddətli yaxşılaşdırmaları uzunmüddətli hədəflərlə birləşdirməyi və Lean, Dafny, Rocq, Agda, Iris kimi alətlərlə əməkdaşlığı davam etdirməyi planlaşdırır. Jane Street bu komanda üçün London və Nyu-Yorkda işçi axtarır.