" Sobre la crueldad de enseñar realmente ciencias de la computación " es un artículo académico de 1988 de EW Dijkstra [1] que sostiene que la programación informática debe entenderse como una rama de las matemáticas y que la demostrabilidad formal de un programa es un criterio importante para su corrección.
A pesar del título, la mayor parte del artículo trata sobre el intento de Dijkstra de colocar la informática en una perspectiva más amplia dentro de la ciencia , y al final se aborda la enseñanza como corolario . Específicamente, Dijkstra hizo una “propuesta para un curso de introducción a la programación para estudiantes de primer año” que consistía en la lógica de Hoare como un sistema formal no interpretado .
Desde que se acuñó el término "ingeniería de software", la verificación formal casi siempre se ha considerado que requiere demasiados recursos para ser factible. [ cita necesaria ] En aplicaciones complejas, la dificultad de especificar correctamente qué debe hacer el programa en primer lugar también es una fuente común de error. Generalmente se emplean otros métodos de prueba de software para tratar de eliminar errores y se consideran muchos otros factores en la medición de la calidad del software .
Hasta el final de su vida, Dijkstra sostuvo que los desafíos centrales de la informática no se habían cumplido a su satisfacción, debido a un énfasis insuficiente en la corrección del programa (aunque sin obviar otros requisitos, como la mantenibilidad y la eficiencia ). [2]
La informática tal como se enseña hoy en día no sigue todos los consejos de Dijkstra. Los planes de estudio generalmente enfatizan técnicas para gestionar la complejidad y prepararse para cambios futuros, siguiendo los escritos anteriores de Dijkstra. Estos incluyen abstracción , programación por contrato y patrones de diseño . Se enseñan como requisitos básicos técnicas de programación para evitar errores y métodos convencionales de prueba de software, y los estudiantes están expuestos a ciertas herramientas matemáticas, pero los métodos de verificación formal no se incluyen en el plan de estudios, excepto quizás como un tema avanzado. [3] Así que, en cierto modo, se han seguido las ideas de Dijkstra; sin embargo, las ideas que más le interesaban no lo han sido.
Los planes de estudios recién formados en ingeniería de software han adoptado las recomendaciones de Dijkstra. El enfoque de estos programas es la especificación formal de los requisitos y el diseño del software para facilitar la validación formal de la corrección del sistema. En Canadá, suelen ser títulos de ingeniería acreditados con competencias básicas similares en ingeniería basada en la física. [4]