A final appplication of logic in computing in general and computer science in particular is in the area of program correctness.  A program is correct when it does what it is intended to do, and it is formally correct if it can be mathematically proven to be correct.

Normally, we use testing methods to determine program correctness.  Suppose that you are asked to write a program that prompts a user for a number and then calculates and displays the square of that number.  Then, once written, you will test the program by inputing a number of numbers and making sure that the number that is displayed is indeed the square of the number that you input.  You may also see what happens when the user enters an illegal input, such as a string. 

While this type of testing is acceptable for many applications, there are cases where you will want to be more certain that the program is correct.  An example might be a routine that controls a nuclear power plant.  For applications such as these, one would like to be able to mathematically prove that the program is correct.

Clearly, in order to be able to formally prove that a program is correct, you need a language in which to specify very precisely what you want the program to achieve, and computer scientists and software engineers have therefore develop a number of fomal specification languages, including Z (pronounced "zed", not "zee") and VDM (http://en.wikipedia.org/wiki/Specification_language).  Most formal specification languages are based on formal logic.