العمليات الاجتماعية، التحقق من البرامج وكل ذلك

في ورقة جدلية (De Millo et al. 1979) في أواخر السبعينيات، جادل ر. أ. دي ميلو، ر. ج. ليبتون، وأ. ج. بيرليس ضد التحقق الرسمي من البرامج، مستندين في الغالب إلى تشبيه مع البراهين في الرياضيات، وعلى وجه الخصوص، مع استحالة اتباع نهج رسمي صارم في هذا التخصص. توفر الإنجازات الحديثة والمبهرة في مجال إثبات النظريات التفاعلية أرضية مثيرة لإعادة النظر النقدية في أطروحاتهم. نعتقد أن الطبيعة الاجتماعية للإثبات وتطوير البرامج أمر لا جدال فيه وحتمي، لكن التحقق الرسمي ليس متناقضًا معه. يجب أن يسعى التحقق الرسمي ليس فقط للتعامل مع، بل لتسهيل وتعزيز الطبيعة التعاونية والعضوية لهذه العملية، مما يساعدنا في النهاية على السيطرة على التعقيد المتزايد للمعرفة العلمية.