Jane Street 25-წლიანი სკეპტიციზმის შემდეგ ფორმალური მეთოდების გუნდს აყალიბებს

მეოთხედი საუკუნის განმავლობაში Jane Street-ის პოზიცია ფორმალურ მეთოდებზე მარტივი იყო: არ გვაინტერესებს. სატრეიდინგო კომპანიის ბლოგზე გამოქვეყნებულ ახალ პოსტში ეს პოზიცია შეიცვალა. „25 წლის განმავლობაში ვუმბობდი ხალხს, რომ Jane Street-ს, როგორც ორგანიზაციას, ფორმალური მეთოდები უბრალოდ არ აინტერესებდა", — წერს ავტორი. — „ახლა ამას აღარ ვამბობ".

რატომ იყო სკეპტიციზმი გონივრული

პოსტი ხაზგასმით აღნიშნავს, რომ ძველი პოზიცია აშკარად მცდარი არ იყო. Jane Street აქტიურად იყენებს კოდის ხარისხის გასაუმჯობესებელ ინსტრუმენტებს, ხოლო ტიპების სისტემა თავად ფორმალური მეთოდების მსუბუქი ფორმაა, რომლისგანაც კომპანიას დიდი სარგებელი აქვს. თუმცა სრული ვერიფიკაციის ხარჯები იშვიათად მართლდებოდა განსაკუთრებული შემთხვევების გარეთ, მაგალითად ტექნიკის სინთეზის დროს. კლასიკური მაგალითია seL4 — ფორმალურად დამოწმებული მიკრობირთვი და ნამდვილი მიღწევა: 8 700 სტრიქონი C კოდის დასამოწმებლად დაახლოებით 25 ადამიანი-წელი დასჭირდა, სადაც თითო სტრიქონზე დაახლოებით 23 სტრიქონი მტკიცებულება და ნახევარი ადამიანი-დღე მიდიოდა.

ასეთი ხარჯი შეიძლება გამართლდეს უსაფრთხოებისთვის კრიტიკულ მიკრობირთვზე, მაგრამ არა პროგრამული უზრუნველყოფის უმეტესობისთვის — კომპანიის აზრით, არც მისი ყველაზე კრიტიკული სისტემებისთვის. შემდეგ აგენტური პროგრამირება გამოჩნდა.

რა შეცვალა აგენტურმა პროგრამირებამ

ჯერ ხარჯის მხარე შეიცვალა: მოდელებს დამოუკიდებლად რთული მტკიცებულებების აწყობა არ შეუძლიათ, აღნიშნავს ავტორი, მაგრამ ისინი რუტინულ ნაწილს ავტომატიზებენ და ამ ინსტრუმენტებს გაცილებით მეტ ადამიანს აძლევენ ხელში, რაც ძველ გათვლას ცვლის.

სარგებლის მხარეც შეიცვალა. მოდელები კარგად აღწევენ დასახულ მიზანს, მაგრამ უარესად ინარჩუნებენ კოდბაზის ჯანმრთელობას და შედეგი სლოპისკენ იხრება: ზედმეტად გართულებული, უცნაური შეცდომებითა და კიდური შემთხვევებით სავსე, ხშირად კოდბაზის არსებითი ინვარიანტების დამრღვევი. ამიტომ ვერიფიკაციის ბარიერი უფრო ძვირია, ვიდრე ოდესმე, ხოლო მტკიცებულება უკუკავშირის ძლიერი ფორმაა, რომელიც აგენტებს სჭირდებათ — როგორც RL-ის წვრთნისას, ისე ყოველდღიურ პროგრამირებაში.

ტესტები ღირებულია — Jane Street მიუთითებს property-based ტესტებსა და fuzzing-ზე — მაგრამ მთელ მდგომარეობათა სივრცეს ვერ ფარავს. ტიპების სისტემა სამაგიეროდ უნივერსალურ გარანტიებს იძლევა: მონაცემთა რბოლის გამომრიცხავი სისტემა მათ მთლიანად აღმოფხვრის, ხოლო cross-site scripting-ის შეუძლებლობას ტიპები კატეგორიულად უზრუნველყოფს. გამონაკლისები, როგორიცაა Obj.magic, არსებობს, მაგრამ მათი თვალთვალი და აკრძალვა შეიძლება.

რატომ საკუთარი გუნდი

Jane Street ამტკიცებს, რომ ამ საქმისთვის უჩვეულოდ კარგ პოზიციაშია: მას ეკუთვნის OxCaml — OCaml-ის საკუთარი ვარიანტი — რაც ენის დამტკიცებაზე ორიენტირებული ტექნიკისთვის მორგებას აძლევს საშუალებას: მოდულური სპეციფიკაციები ტიპების სისტემაში, ტიპის დონეზე შეზღუდვები მფლობელობასა და ცვლადობაზე, დამტკიცების მეთოდები თავად ენაში. მომხმარებლებს ეს ფუნქციები სურთ — პოსტში ნათქვამია, რომ ისინი ჩივიან დაპირებული ტიპური ფუნქციების შენელებაზე, ხოლო პროგრამირების ენების კვლევაში ყველაზე რთული ახალი იდეების რეალურ სამუშაოში გამომყენებლის პოვნაა.

გუნდი გეგმავს მყისიერი ეფექტის გაუმჯობესებებსა და გრძელვადიან მიზნებს, და აპირებს თანამშრომლობას Lean-თან, Dafny-სთან, Rocq-თან, Agda-სთან და Iris-თან. Jane Street ამ გუნდისთვის ლონდონსა და ნიუ-იორკში ადამიანებს ეძებს.