Another Position Paper on "Fairness"
Fred B. Schneider, Leslie Lamport · Software Engineering Notes · 2016
The argument of [2] can be summarized as follows. An obligation is considered void if it is impossible to detect that the obligation has not been fulfilled. Any property of program execution that cannot be checked by performing finite experiments is, therefore, a void obligation. A specification, being a contract between implementor and user, should not contain clauses that cannot be enforced. Therefore, void obligations should not appear in specifications, since there would be no way to determine whether or not an implementation satisfies void obligations in the specification. Obligations that should not appear in specifications can be ignored with impunity.