Barrapunto

A Dijkstra le molaba la verificación formal. Y su buena razón tiene. El problema reside en que es caro de cojones verificar formalmente un programa de chorricientas mil líneas de código.

En realidad, más que "verificación formal" (que significa comprobar formalmente que un programa es correcto), lo que propone es la "construcción formal", esto es, construir el programa (derivar una formula), a partir de su especificación (otra fórmula).

Y claro que esto es costoso: tanto para enseñarlo como para aplicarlo. Y la realidad es que en la actualidad, los métodos formales no están desarrollados lo suficiente como para el tipo de sistemas que requerimos. Pero que, por el estado actual de la ciencia, hoy no pueda hacerse (o porque sea muy costoso) no significa que la cosa no sea así (eso es lo que molesta a más de uno, y por lo que tantos se niegan a ver).