Heh, one of my lecturers was ranting about the millions wasted on research grants for testing methodologies when it's proven that they can't formally confirm program correctness. Old Edsger had a lot of foresight in that respect. Still, he's gloriously ambiguous about what he considers a 'modest and elegant programming language'.