جين ستريت تُنشئ فريقاً للأساليب الشكلية بعد 25 عاماً من التشكيك

طوال ربع قرن كان موقف شركة جين ستريت من الأساليب الشكلية بسيطاً: لا نهتم بها. وفي مقال جديد على مدونة شركة التداول تغيّر هذا الموقف. يكتب المؤلف: "طوال 25 عاماً كنت أقول للناس إن جين ستريت كمنظمة لا تهتم بالأساليب الشكلية. لم أعد أقول ذلك".

لماذا كان التشكيك معقولاً

يحرص المقال على التوضيح أن الموقف القديم لم يكن خاطئاً بشكل واضح. تستخدم جين ستريت بكثافة أدوات تحسّن جودة الكود، وأنظمة الأنواع نفسها شكل خفيف من الأساليب الشكلية استفادت منه الشركة كثيراً. لكن التحقق الكامل كان يحمل تكاليف نادراً ما تستحق خارج حالات خاصة مثل تخليق العتاد. والمثال الكلاسيكي هو seL4، نواة دقيقة مُتحقَّق منها شكلياً وإنجاز حقيقي: تطلّب التحقق من 8700 سطر بلغة C نحو 25 سنة-شخص، إذ احتاج كل سطر إلى نحو 23 سطر إثبات ونصف يوم عمل.

قد تكون هذه المقايضة مجدية في نواة دقيقة حساسة أمنياً. لكنها لم تبدُ مجدية لمعظم البرمجيات، ولا حتى لأكثر أنظمة الشركة حساسية — إلى أن ظهر الترميز الوكيلي.

ما غيّره الترميز الوكيلي

تغيّر جانب التكلفة أولاً. لا تستطيع النماذج وحدها بناء إثباتات صعبة، كما يلاحظ المؤلف، لكنها تؤتمت قدراً كبيراً من العمل الممل وتجعل هذه الأدوات متاحة لعدد أكبر بكثير من الناس، ما يغيّر حساب الكلفة والعائد القديم.

وتغيّر جانب العائد أيضاً. النماذج تتحسن في كتابة كود يحقق هدفاً محدداً، لكنها أضعف في الحفاظ على صحة قاعدة الكود، والنتيجة تميل إلى "الرداءة": تعقيد مفرط، وأخطاء غريبة وحالات حدّية، وانتهاك للثوابت الأساسية التي تعتمد عليها بقية الشيفرة. وهذا يجعل عنق زجاجة التحقق أكثر كلفة من أي وقت مضى، والأساليب الشكلية مرشحة لتخفيفه. كما تحتاج الوكلاء إلى تغذية راجعة — في التدريب بالتعلم المعزز وفي الترميز اليومي — والإثباتات شكل قوي منها.

تبقى الاختبارات مهمة — تستثمر جين ستريت بكثافة في بنية الاختبار وتشير إلى الاختبارات القائمة على الخصائص والـfuzzing — لكنها لا تغطي كامل فضاء الحالات. أما أنظمة الأنواع فتمنح ضمانات شاملة: نظام يمنع تسابقات البيانات يزيلها كلها، وأنواع تجعل هجمات الحقن عبر المواقع مستحيلة تفعل ذلك بشكل قاطع. توجد منافذ هروب مثل Obj.magic، لكن يمكن تتبعها وحظرها أو إثبات أنها آمنة. وهذه التجربة هي ما يشجع الشركة على تبني تقنيات إثبات أقوى.

لماذا يُبنى الأمر داخلياً

ترى جين ستريت أنها في موقع ممتاز لهذا العمل: فهي تتحكم بـ OxCaml، نسختها الخاصة من OCaml، ما يسمح بتشكيل اللغة لتقنيات الإثبات — مواصفات معيارية داخل نظام الأنواع، وقيود على مستوى النوع تتعلق بالملكية والتحويل، وأساليب إثبات مدمجة في اللغة نفسها. ولديها أيضاً قاعدة مستخدمين تريد ذلك: يذكر المقال أن المستخدمين يشتكون بانتظام من أن ميزات الأنواع الموعودة لا تصل بالسرعة الكافية، وأن الجزء الصعب في أبحاث لغات البرمجة هو إيجاد من يستخدم الأفكار في عمل حقيقي.

تخطط الفرقة لدمج تحسينات قصيرة الأمد ذات أثر فوري مع أهداف طويلة الأمد وطموحة، وتنوي مواصلة التفاعل مع أدوات خارجية مثل Lean وDafny وRocq وAgda وIris. وتوظف جين ستريت لهذه الفرقة في لندن ونيويورك، والمقابلات في مرحلة مبكرة.