October, Week 7

This week's emphasis was on program correctness. To prove that a program works, precondition=>post-condition must be proved, but in order to prove it one has to consider every possible case, and every possible branch that a program can follow. I think that a formal proof of program correctness is not very practical in the real world, for the very same reason described above. If a program is simple recursive function, then it is easy to prove its correctness using formal proof. However, because of its simplicity, I don't see a need of proving it correct, because
it is easy to say whether a simple function works or not just by looking at the code. It would take less time to write a program, proofread the code 5 times, think of every possible scenario (it is possible, because the function is really simple), and test it on some value, rather then take a pencil and prove it. If a function is big, however, the proof will be too complex anyways. Even something as simple as recursive binary search took 2 whole slides to prove during the lecture (and only 1st part of the proof).