Control Predicates Are Better than Dummy Variables for Representing Program Control - Lamport, Leslie (ACM Transactions on Programming Languages and Systems. Also appeared as SRC Research Report 11., 1988)
This paper describes an example I came across in which the explicit control predicates introduced in [47] lead to a simpler proof than do dummy variables. This example served as an excuse. The real reason for publishing it was to lobby for the use of control predicates. There used to be an incredible reluctance by theoretical computer scientists to mention the control state of a program. When I first described the work in [40] to Albert Meyer, he immediately got hung up on the control predicates. We spent an hour arguing about them–I saying that they were necessary (as was first proved by Susan in her thesis), and he saying that I must be doing something wrong. I had the feeling that I was arguing logical necessity against religious belief, and there's no way logic can overcome religion.