Jane Street-ը 25 տարվա թերահավատությունից հետո ֆորմալ մեթոդների թիմ է կազմում

Չորս դարի քառորդի ընթացքում Jane Street-ի դիրքորոշումը ֆորմալ մեթոդների նկատմամբ պարզ էր՝ մեզ դա չի հետաքրքրում։ Առևտրային ընկերության բլոգում հրապարակված նոր գրառման մեջ այդ դիրքորոշումը փոխվել է։ «Վերջին 25 տարվա ընթացքում մարդկանց ասում էի, որ Jane Street-ը որպես կազմակերպություն պարզապես չի հետաքրքրվում ֆորմալ մեթոդներով»,— գրում է հեղինակը։ «Հիմա այդպես չեմ ասում»։

Ինչու թերահավատությունը հիմնավորված էր

Գրառումը հատուկ նշում է, որ հին դիրքորոշումը ակնհայտորեն սխալ չէր։ Jane Street-ը ակտիվորեն օգտագործում է կոդի որակը բարելավող գործիքներ, իսկ տիպերի համակարգերն իրենք ֆորմալ մեթոդների թեթև ձև են, որից ընկերությունը մեծ օգուտ է ստացել։ Սակայն ամբողջական վերիֆիկացիայի ծախսերը հազվադեպ էին արդարացվում հատուկ դեպքերից դուրս, օրինակ՝ սարքային սինթեզի։ Դասական օրինակը seL4-ն է՝ ֆորմալ ստուգված միկրոմիջուկ և իսկական ձեռքբերում. 8 700 տող C կոդ ստուգելու համար պահանջվեց մոտ 25 մարդ-տարի, որտեղ ամեն տողի համար մոտ 23 տող ապացույց և կես մարդ-օր էր անհրաժեշտ։

Նման հաշվեկշիռը կարող է արդարացված լինել անվտանգության համար կրիտիկական միկրոմիջուկի դեպքում, բայց ոչ ծրագրային ապահովման մեծ մասի, և ընկերության կարծիքով՝ նաև ոչ իր ամենակրիտիկական համակարգերի համար։ Հետո եկավ ագենտային ծրագրավորումը։

Ինչ փոխեց ագենտային ծրագրավորումը

Նախ փոխվեց ծախսի կողմը. մոդելները ինքնուրույն չեն կարող կամայական բարդ ապացույցներ կառուցել, նշում է հեղինակը, բայց ավտոմատացնում են ձանձրալի աշխատանքի մեծ մասը և այդ գործիքները հասանելի են դարձնում շատ ավելի մարդկանց, ինչը փոխում է հին հաշվարկը։

Փոխվեց նաև օգուտի կողմը։ Մոդելները լավ են հասնում դրված նպատակին, բայց ավելի վատ են պահպանում կոդբազի առողջությունը, և արդյունքը հակված է «slop»-ին. չափազանց բարդ, տարօրինակ սխալներով ու եզրային դեպքերով լի, հաճախ կոդբազի էական ինվարիանտները խախտող։ Դա վերիֆիկացիայի խցանումը դարձնում է ավելի թանկ, քան երբևէ, իսկ ապացույցները ուժեղ հետադարձ կապ են, որն ագենտներին պետք է և՛ RL ուսուցման, և՛ առօրյա ծրագրավորման ժամանակ։

Թեստերը արժեքավոր են. Jane Street-ը մատնանշում է property-based թեստերը և fuzzing-ը, սակայն դրանք չեն ընդգրկում ամբողջ վիճակային տարածությունը։ Տիպերի համակարգերը փոխարենը ունիվերսալ երաշխիքներ են տալիս. տվյալների մրցավազքը բացառող համակարգը վերացնում է դրանք ամբողջությամբ, իսկ cross-site scripting-ը անհնար դարձնող տիպերը դա անում են կատեգորիկ։ Obj.magic-ի նման ելքեր կան, բայց դրանք կարելի է հետևել ու արգելել։

Ինչու սեփական թիմ

Jane Street-ը պնդում է, որ անսովոր լավ դիրքում է. ընկերությանը պատկանում է OxCaml-ը՝ OCaml-ի իր տարբերակը, ինչը թույլ է տալիս լեզուն հարմարեցնել ապացուցման տեխնիկաներին. մոդուլային սպեցիֆիկացիաներ տիպերի համակարգում, տիպի մակարդակի սահմանափակումներ սեփականության ու փոփոխականության վրա, ապացուցման մեթոդներ հենց լեզվում։ Օգտվողներն ուզում են դա. գրառման մեջ նշվում է, որ նրանք դժգոհում են խոստացված տիպային հատկությունների դանդաղությունից, իսկ լեզուների հետազոտություններում ամենադժվարը նոր իդեաները իրական աշխատանքում օգտագործող մարդ գտնելն է։

Թիմը ծրագրում է կարճաժամկետ բարելավումներ և երկարաժամկետ նպատակներ, ինչպես նաև համագործակցություն Lean-ի, Dafny-ի, Rocq-ի, Agda-ի ու Iris-ի հետ։ Jane Street-ը մարդկանց փնտրում է Լոնդոնում և Նյու Յորքում։