لقد كان لدي منذ فترة طويلة نقطة ضعف تجاه اللغات المكتوبة بشكل تابع مثل Coq Rocq و Lean. إنها توفر إمكانية وجود نظام كتابة قادر على تشفير وتنفيذ الثوابت الدقيقة بشكل تعسفي. هذا النوع من الأشياء، في اللغات العادية، ينتهي به الأمر (في أحسن الأحوال) كتعليق، والذي سرعان ما يضيع مع نمو حجم الفريق. ثم تحصل على سوء فهم دقيق ومكونات لا تتناسب تمامًا مع بعضها البعض. غالبًا ما تكون هذه المكونات قد نمت إلى حجم كافٍ، وعندما يتم ملاحظة المشكلة، فإن محاذاة أي منهما يكون احتمالًا مرهقًا. ربما، على سبيل المثال، الأنواع التابعة بطريقة مغرية، يمكنك كتابة تلك الثوابت بشكل رسمي وجعل الآلة تتحقق منها.
(ملاحظة: غيرت Coq اسمها! أتذكر قبل سنوات عديدة في مؤتمر Coq في برينستون، حاولت أن أشير إلى أنه في العالم الناطق باللغة الإنجليزية، فإن وجود لغة برمجة تسمى Coq كان عائقًا. لا أعتقد أن الجمهور وافق على ذلك في ذلك الوقت. ومازحت أيضًا أن العديد من المحادثات هناك بدت وكأنها خطاب لتيريون لانيستر، حيث كان هناك الكثير من Coqs وHoares. نكتة كانت مضحكة وفي الوقت المناسب، على الرغم من أنها سقطت مسطح تمامًا، ويأتي كما حدث قبل الموسم الأخير من هذا العرض وما نحتفظ به من ذاكرتنا الجماعية.)
كانت المشكلة دائمًا هي أنه مع قوة نظام الكتابة الكبيرة يأتي جهد إثبات كبير. يمكنني بالتأكيد أن أشهد على أيام كاملة أمضيتها في إثبات أشياء بسيطة جدًا. يعد إجراء البراهين أمرًا ممتعًا للغاية: فهو يمثل تحديًا وتفاعليًا، كما أن هناك هدفًا واضحًا. لكن يا إلهي، هل يستغرق الأمر الكثير من الوقت، خاصة إذا كنت، مثلي، لا تعرف ما تفعله. هناك أيضًا التجربة الدورية والمزعجة، في نهاية ساعات طويلة من الجهد، حيث تدرك أن الهدف الذي تحاول إثباته هو في الواقع خطأ. النتيجة الكلاسيكية هنا هي بأثر رجعي من جهود seL4 التي وجدت أنه على الرغم من أن المشروع كان كبيرًا بما يكفي ليتمكن المهندسون من تطوير خبرة كبيرة، فقد أمضوا حوالي 10 أضعاف الوقت الذي قضوه في التصميم والتنفيذ في الإثبات. لقد انتهى بهم الأمر إلى الحصول على أكثر من 20 ضعفًا من أسطر كود الإثبات التي حصلوا عليها في كود C.
هذا الحمل الزائد جعل البرمجة باللغات المكتوبة بشكل مستقل متخصصة للغاية. كما حفز الناس أيضًا على محاولة تشغيله تلقائيًا. المحاولة التي أعرفها تمامًا هي F*، حيث يحاول النظام جعل أداة حل SMT تفي بالالتزامات تلقائيًا. من المؤكد أن هذا ينجح في الحالات البسيطة، ولكن من السهل جدًا صياغة شيء يتسبب في انطلاق محلل SMT إلى الفضاء وتشغيله لساعات، مما يجعلك تتساءل عما إذا كان سينتهي من العمل أم لا. لقد رأيت أن الأشخاص الذين يستخدمون هذه اللغات كثيرًا يجب عليهم تطوير حاسة سادسة لمعرفة ما سيجعل الحل سعيدًا، ثم صياغة كل شيء حول ذلك. يمكن أن يساعد ذلك، لكنه إلى حد ما يحول المشكلة إلى غموض: ينتهي بك الأمر إلى خدمة إله معقد ومتقلب.
والحقيقة الحاسمة هي أنه، على الأقل من الناحية النظرية، بمجرد أن تكون العبارة صحيحة، فإن محتويات دليلها تصبح غير ذات صلة: وجودها فقط هو المهم. هذا ليس صحيحًا تمامًا بسبب عاملين معقدين: أولاً، ما أسمته مجموعة seL4 "هندسة البراهين": الحاجة إلى هيكلة البراهين بحيث يتم تقليل جهد إعادة تنظيمها بعد تغيير التعليمات البرمجية. وثانيًا، يمكن أن تؤدي البراهين المعقدة بما فيه الكفاية إلى تفجير أدوات التحقق من الكتابة واستهلاك كميات هائلة من الذاكرة.
لدينا الآن شهادات LLM التي تعد، إلى جانب عدم ملاءمة الإثبات، بأن تكون شكلاً قادرًا للغاية من أشكال أتمتة الإثبات. مع وجود كميات كافية من الأتمتة، ربما لا داعي للقلق بشأن هندسة الإثبات تقريبًا. لا تزال بحاجة إلى تجنب تفجير مدقق النوع، ولكن في اختباراتي المحدودة، يمكن لـ LLMs تجنب ذلك. من المحتمل أن طلاب ماجستير إدارة الأعمال فجأة يجعلون أنظمة النوع التابع أكثر عملية بشكل كبير. كنت أرغب في تجربة هذا الأمر، لذا صممت أداة إلغاء الضغط Zstandard في Lean، ويرجع ذلك في الغالب إلى أنني كنت مهتمًا أيضًا بـ Zstandard.