the programmer's task is not just to write down a program, but that his main task is to give a formal proof that the program he proposes meets the equally formal functional specification As computers become ever more powerful, the job becomes to de-program the error states, to prove that the intended outcome will happen (rather than the unintended outcome)
On the cruelty of really teaching computing science
from University of Texas in Austin
