2015: I consider a concrete case to motivate the distinctions made here. Suppose that I need to write a program that, among other things, must compute the area of the intersection of two polygons. I find on the net a program, inter, that claims to do just that. My program must do other even more critical things. It would be bad if I got the wrong area. It would be much worse if other parts of the program were compromised which might happen if the routine inter were to store anywhere other than its own stack frame. inter’s signature promises just that but it is written in C. Another worse thing is for one of the polygons delivered to inter were delivered further to some program outside the current memory space, exfiltrated. Yet another would be if data not furnished to inter were exfiltrated. These latter ‘worse things’ are bad in part because I may never become aware of them. They may occur without the signals that would lead to fixing the flaw.
I need to prove that much worse things will not happen.