Think about the process of writing, testing and debugging a reasonably complicated program. Let's suppose we have a program written in Java (or Python, or JavaScript, or C, or whatever your favorite language is). The first thing we might try to do is to compile the program, but chances are the program will contain several syntactic errors, and won't compile right off. (Syntactic errors are those that violate the rules of the language — misspellings, missing parentheses, missing semi-colons, etc.) Compilers are good at finding those errors, so it doesn't take long to actually get the program to run.
Now we are interested in whether the program gives the correct results for various sets of test data. If, for some set of data the program halts normally, but gives incorrect results, then the program is said to have a logical error. Even if the program does work properly for all sets of test data, this does not mean that all logical errors have been eliminated. It is normally impossible to test all possible data sets, and although by choosing good test data we can make the probability of error small, we can't be sure that the program is correct. (There are numerous examples of commercial software that have subtle, and sometimes serious, errors that are found by users.) In general, program verification requires the use of formal proof techniques like those we have studied.
A proof that a program is correct consists of two parts. The first part shows that the correct answer is obtained if the program terminates. This part establishes partial correctness of the program. The second part of the proof shows that the program always terminates.