في عالم علوم الحاسوب، هناك توتر مستمر بين مدى المرونة التي يمكن أن تتمتع بها لغة البرمجة وبين مدى أمان استخدامها. يرغب المبرمجون في لغات تسمح لهم ببناء أنظمة معقدة وديناميكية حيث يمكن للوظائف تغيير سلوكها في اللحظة المناسبة، تمامًا مثل السكين السويسري الذي يكيف أدواته حسب المهمة المطلوبة. ومع ذلك، غالبًا ما تأتي هذه المرونة بتكلفة: إذ يصبح من الصعب للغاية التنبؤ بما سيفعله البرنامج فعليًا عند تشغيله. هل سينهي مهمته، أم سيعلق في حلقة مفرغة لا نهاية لها؟ هل سيتعطل، أم سينتج النتيجة الصحيحة؟ لعقود من الزمن، طور الباحثون أنظمة تسمى "أنظمة الأنواع" (type systems) لتعمل كشبكة أمان، حيث تتحقق من الكود قبل تشغيله لضمان اتباعه للقواعد المنطقية. ومن بين هذه الأنظمة، أثبت نهج محدد يُعرف باسم "النمذجة بالتقاطع" (intersection typing) قوة كبيرة في تحليل كيفية تصرف البرامج، لكنه واجه تاريخيًا صعوبات عند تطبيقه على ميزات البرمجة الحديثة التي تسمح للمطورين باعتراض الأحداث غير المتوقعة وإدارتها، والتي تُعرف بـ "التأثيرات" (effects).

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

لفهم المشكلة، يجب على المرء أولاً النظر في كيفية تعامل البرامج الحديثة مع "التأثيرات". في الحوسبة التقليدية، غالبًا ما يُنظر إلى البرنامج كصندوق مغلق يأخذ مدخلات وينتج مخرجات. ولكن في الواقع، غالبًا ما تحتاج البرامج للقيام بأشياء مثل قراءة ملف، أو انتظار نقرة مستخدم على زر، أو اتخاذ قرار عشوائي. تُسمى هذه "التأثيرات الجبرية" (algebraic effects). في الأنظمة القديمة، كانت قواعد كيفية سلوك هذه التأثيرات مدمجة في اللغة. أما في الأنظمة الأحدث، فقد مُنح المبرمجون القدرة على تحديد قواعدهم الخاصة؛ حيث يمكنهم كتابة "معالج" (handler) يعترض التأثير، ويقرر ما يجب فعله معه، ثم يواصل البرنامج عمله. هذه القوة مذهلة، فهي تسمح بميزات مثل التراجع عن الأفعال، أو محاكاة نتائج مختلفة، أو إدارة تدفقات البيانات المعقدة. ومع ذلك، تأتي هذه القوة مع خطر خفي: نظرًا لأن المعالج يمكنه تغيير مسار البرنامج بطرق عديدة، يصبح من المستحيل تقريبًا استخدام الأدوات الرياضية القياسية لإثبات أن البرنامج سيتوقف عن العمل أبدًا أو أنه سيصل إلى حالة مرغوبة. وقد أظهرت الأبحاث السابقة أنه بالنسبة لهذه الأنظمة المتقدمة، فإن مشكلة التحقق مما إذا كان البرنامج يمكنه الوصول إلى نتيجة معينة هي مشكلة "غير قابلة للتقرير" (undecidable)، مما يعني أنه لا توجد خوارزمية حاسوبية يمكنها حلها لكل الحالات الممكنة.

لقد سعى مؤلفو هذه الورقة لتغيير ذلك. بدأوا بتطوير نظام أنواع جديد، أطلقوا عليه اسم HEBI. وببساطة، نظام الأنواع هو مجموعة من القواعد التي تخصص "تسمية" (label) لكل جزء من الكود، تصف ما يُسمح لهذا الجزء بفعله. الابتكار هنا هو أن تسمياتهم هي تسميات "سلوكية". فبدلاً من مجرد القول "هذه الوظيفة تأخذ رقمًا وتعيد رقمًا"، يصف نظامهم القصة الكاملة للحوسبة؛ فهو يسجل ترتيب حدوث التأثيرات، والقيم التي يتم تمريرها إليها، وكيف يعتمد مستقبل البرنامج على نتائج تلك التأثيرات. تخيل برنامجًا يطلب من المستخدم اختيارًا، وبناءً على ذلك الاختيار، يقوم بأحد إجراءين مختلفين. النظام الجديد لا يكتفي بملاحظة أنه تم اتخاذ قرار، بل يرسم خريطة لشجرة الاحتمالات بأكملها، متتبعًا كل فرع يمكن أن يتخذه البرنامج. ومن خلال القيام بذلك، أنشأوا نظامًا دقيقًا بما يكفي لالتقاط السلوك الدقيق للبرنامج، بما في ذلك كيفية التعامل مع المقاطعات والاستئناف.

إن الاكتشاف الرئيسي الأول للورقة هو أن هذا النظام الجديد دقيق للغاية. فقد أثبت الباحثون أنه إذا أمكن إعطاء تسمية لبرنامج ما في نظامهم، فمن المضمون أن ينهي عمله. وعلى العكس من ذلك، إذا كان البرنامج مضمون الإنهاء، فيمكن دائمًا إعطاؤه تسمية في نظامهم. وهذه خاصية نادرة وقوية في علوم الحاسوب، تُعرف بـ "توصيف الإنهاء" (characterizing termination). وهذا يعني أن النظام يميز بدقة بين البرامج التي ستعمل للأبد وتلك التي ستتوقف. لقد حققوا ذلك من خلال تكييف تقنية رياضية كلاسيكية لتعمل مع تسمياتهم السلوكية الجديدة، مما أظهر أن النظام قوي بما يكفي للتعامل مع التفاعلات المعقدة بين المعالجات والتأثيرات التي تديرها. وهذا يثبت أن عدم قابلية التقرير في الأنظمة السابقة لم يكن عيبًا متأصلًا في نمط البرمجة نفسه، بل كان محدودية في الأدوات المستخدمة لتحليله.

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

كانت نتيجة هذا التبسيط بمثابة طفرة. فقد أثبت البباحثون أنه بالنسبة لهذا النظام الأبسط، فإن مشكلة التحقق مما إذا كان البرنامج يمكنه الوصول إلى نتيجة معينة هي مشكلة "قابلة للتقرير" (decidable). وهذا يعني أن الحاسوب يمكنه الآن التحقق تلقائيًا مما إذا كان برنامج مكتوب بهذا الأسلوب سيصل إلى حالة مرغوبة. ويمثل هذا تحولًا كبيرًا عن الحالة السابقة، حيث كان من المعروف أن مثل هذا التحقق مستحيل للأنظمة المشابهة. وكان مفتاح هذا النجاح هو إدراك أن الطبيعة السلوكية المعقدة لنظامهم الأصلي يمكن استخدامها كـ "تحسين" (refinement) لنظامهم الأبسط. لقد أظهروا أن كل برنامج يتوافق مع قواعد HEB البسيطة يمكن ربطه بمجموعة محددة ومتناهية من الأوصاف في نظام HEBI المعقد. ولأن هذه المجموعة متناهية، يمكن للحاسوب البحث فيها بشكل شامل للعثور على الإجابة.

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

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

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