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

FROM:University of Texas in AustinOn the Cruelty of Really Teaching Computing Science

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)

Josh Beckman