Processus sociaux, vérification de programmes et tout le reste

Dans un article controversé (De Millo et al. 1979) à la fin des années 1970, R. A. De Millo, R. J. Lipton et A. J. Perlis s'opposaient aux vérifications formelles des programmes, motivant principalement leur position par une analogie avec les preuves en mathématiques et, en particulier, avec l'impraticabilité d'une approche strictement formaliste de cette discipline. Les réalisations récentes et impressionnantes dans le domaine de la démonstration interactive de théorèmes fournissent un terrain intéressant pour une réévaluation critique de leurs thèses. Nous croyons que la nature sociale de la preuve et du développement de programmes est incontestable et inéluctable, mais que la vérification formelle n'y est pas antithétique. La vérification formelle devrait s'efforcer non seulement de faire face à, mais aussi de faciliter et d'améliorer la nature collaborative et organique de ce processus, aidant finalement à maîtriser la complexité croissante de la connaissance scientifique.