¿Es TDD la hermana pequeña de la validación formal?

Hace un tiempo, al crear el grupo de TDD en castellano, hacía esta pregunta del título. ¿Es TDD la hermana pequeña de la validación formal? Hay un artículo del gran E. W. Dijkstra, "Sobre la crueldad de verdaderamente enseñar ciencias de la computación" que me parece muy revelador tal y como hoy entendemos la ingeniería del software, y cómo se veían las cosas hace tan solo poco más de 20 años.
Básicamente Dijkstra proponía enseñar a los estudiantes de informática, como introducción en el primer curso, la validación formal de los programas sin siquiera tocar un ordenador para programar. Bastante sorprendente.
¿podremos un día verificar formalmente que un programa hace lo que esperamos que haga, y nada más? Lo que pasa, que el principal problema no es verificar, si no CONOCER, aprender, asimilar, conceptualizar lo que tiene que hacer.
Os dejo con este video, del 2001, con una pequeña entrevista a tan interesante personalidad.

Podeis encontrar todos sus manuscritos, algunos de ellos traducidos a castellano en la universidad de Texas.

Computer science is no more about computers
than astronomy is about telescopes

E. W. Dijkstra

Siempre me ha intrigado el verdadero sentido de esa frase...