Procesos sociales, verificación de programas y todo eso

En un artículo controvertido (De Millo et al. 1979) a finales de los años 70, R. A. De Millo, R. J. Lipton y A. J. Perlis argumentaron en contra de las verificaciones formales de programas, motivando su posición principalmente con una analogía con las demostraciones en matemáticas y, en particular, con la impracticabilidad de un enfoque estrictamente formalista en esta disciplina. Los recientes e impresionantes logros en el campo de la demostración interactiva de teoremas proporcionan una base interesante para una revisión crítica de sus tesis. Creemos que la naturaleza social de la demostración y el desarrollo de programas es innegable e ineludible, pero la verificación formal no es antitética a ello. La verificación formal debería esforzarse no solo en manejar, sino en facilitar y potenciar la naturaleza colaborativa y orgánica de este proceso, ayudándonos finalmente a dominar la complejidad creciente del conocimiento científico.