ג'יין סטריט משנה כיוון אחרי 25 שנות ספקנות ותבנה צוות לשיטות פורמליות

במשך רבע מאה עמדת ג'יין סטריט בנוגע לשיטות פורמליות הייתה פשוטה: לא מעוניינים. בפוסט חדש בבלוג של חברת המסחר הזה עמדה זו השתנתה. "במשך 25 השנים האחרונות אמרתי לאנשים שג'יין סטריט כגוף פשוט לא מתעניינת בשיטות פורמליות", כותב המחבר. "אני כבר לא אומר את זה".

מדוע הספקנות הייתה סבירה

הפוסט מקפיד לציין שהעמדה הישנה לא הייתה שגויה בעליל. ג'יין סטריט משתמשת רבות בכלים לשיפור איכות הקוד, ומערכות טיפוסים הן בעצמן סוג של שיטה פורמלית קלה שממנה הפיקה החברה תועלת עצומה. אבל אימות מלא נשא עלויות שלעיתים רחוקות היו משתלמות מחוץ למקרים מיוחדים כמו סינתזת חומרה. הדוגמה הקלאסית היא seL4, מיקרו-קרנל מאומת פורמלית והישג של ממש: אימות 8,700 שורות C דרש כ-25 שנות אדם, כשכל שורה חייבה כ-23 שורות הוכחה וחצי יום עבודה.

איזון כזה עשוי להשתלם במיקרו-קרנל קריטי לביטחון. הוא לא נראה משתלם לרוב התוכנה, ולפי החברה גם לא למערכות הקריטיות ביותר שלה — עד שהגיע קידוד סוכני.

מה שינה הקידוד הסוכני

צד העלות זז ראשון. מודלים אינם מסוגלים לבנות לבדם הוכחות קשות במיוחד, מציין המחבר, אבל הם מבצעים אוטומטית חלק ניכר מהעבודה המשעממת והופכים את הכלים לזמינים לאנשים רבים יותר, וזה משנה את חשבון העלות-תועלת הישן.

גם צד התועלת זז. מודלים טובים יותר ויותר בכתיבת קוד שמשיג מטרה, אך גרועים בשמירה על בריאות בסיס הקוד, והתוצאה נוטה ל"סלופ": מסובך מדי, מלא באגים מוזרים ומקרי קצה, ולעיתים קרובות מפר אינווריאנטים שהקוד סביבו תלוי בהם. כך צוואר הבקבוק של האימות יקר מתמיד, ושיטות פורמליות הן מועמדת להקל עליו. סוכנים גם זקוקים למשוב — באימון RL ובקידוד יומיומי — והוכחות הן צורה חזקה שלו.

בדיקות נשארות חשובות — ג'יין סטריט משקיעה רבות בתשתית בדיקות ומצביעה על בדיקות מבוססות תכונות ועל fuzzing — אבל הן אינן מכסות את כל מרחב המצבים. מערכות טיפוסים נותנות במקום זאת ערבויות אוניברסליות: מערכת שמונעת מרוצי נתונים מסלקת את כולם, וטיפוסים שהופכים cross-site scripting לבלתי אפשרי עושים זאת באופן קטגורי. פתחי מילוט כמו Obj.magic קיימים, אבל אפשר לעקוב אחריהם ולאסור אותם, או להוכיח שהם בטוחים. הניסיון הזה הוא שמעודד את החברה לאמץ טכניקות הוכחה חזקות יותר.

מדוע לבנות את זה בבית

ג'יין סטריט טוענת שהיא בעמדה טובה במיוחד למשימה. היא שולטת ב-OxCaml, הגרסה שלה של OCaml, מה שמאפשר לעצב את השפה להוכחות — מפרטים מודולריים בתוך מערכת הטיפוסים, אילוצים ברמת הטיפוס על בעלות ומוטציה, ושיטות הוכחה בתוך השפה עצמה. יש לה גם בסיס משתמשים שרוצה את זה: בפוסט נכתב שמשתמשים מתלוננים תדיר שתכונות טיפוסים שהובטחו אינן מגיעות מהר מספיק, ושברוב המחקר בשפות תכנות החלק הקשה הוא למצוא מישהו שמוכן להשתמש ברעיונות בעבודה אמיתית.

הצוות מתכנן שילוב של שיפורים קצרי טווח בעלי השפעה מיידית עם יעדים ארוכי טווח ושאפתניים, ומתכוון להמשיך לשתף פעולה עם כלים חיצוניים כמו Lean, Dafny, Rocq, Agda ו-Iris. ג'יין סטריט מגייסת לצוות בלונדון ובניו יורק, והראיונות בשלב מוקדם.