The future of programming

In the future, computer programs will be written in proof assistants, like Coq and Isabelle. That's because termination is guaranteed, and because we can prove things about programs. For example, we can prove two programs are equivalent. One algorithm might be easy to understand, but slow. The other might be hard to understand, but fast. We need a proof that the latter is equivalent to the former, so we can use the faster algorithm instead. Also, proofs involving programs can be used to perform peephole optimization. That is, expressions within the program can be transformed according to theorems established by the proof assistant.