The program that performs the computation is equivalent to the proof of the theorem. By proving the theorem the program is guaranteed to be correct.
It is not that simple, of course, but so promising is type theory that since 1989 the EU has been funding a string of projects to develop it under the Future and Emerging Technologies programme.
That style of working is going to change so that we spend more effort on actually writing programs than testing them.

Thanks for the clip, this is extremely interesting.
According to Gödel's incompleteness theory there are mathematical theorems which are true, but cant be proven to be so.
So there will be computer programs that can not be dealt with in this fashion.