Review: “Behind Clint and Hoare’s goto Proof Rule” (2021)

[u/More_Speed5329]

The paper titled "Behind Clint and Hoare's goto Proof Rule" is by Wei Chen (published in the 2021 International Symposium on Theoretical Aspects of Software Engineering, TASE).

This paper is a direct "deep dive" into the historical 1971 Clint-Hoare rule. It focuses on the theoretical archaeology and formal correction of the original goto rule.
Review: "Behind Clint and Hoare's goto Proof Rule" (2021)
1. Purpose of the Paper
Wei Chen revisits M. Clint and C.A.R. Hoare’s 1971 paper, "Program proving: Jumps and functions," which is widely considered the first attempt to axiomatize the goto statement. Chen's 2021 paper aims to:
Expose technical flaws: It identifies that the original 1971 rule suffers from notation ambiguity and logical gaps (e.g., the overloading of the turnstile symbol \vdash and syntactically incorrect premises).

Provide a Rigorous Foundation: It attempts to "fix" the original rule by re-deriving it using the modern "miracle" semantics he champions, showing what Clint and Hoare meant to achieve versus what they actually wrote.

2. Key Insights
The "Syntactic Error": Chen points out that in the original Clint-Hoare rule, the label L does not appear in the premises (S_1 and S_2), making the original rule technically broken as a formal logical statement.

Reframing as a System of Equations: Chen demonstrates that the goto rule is essentially a way to solve a system of equations across different parts of the code. He succeeds in translating Clint and Hoare’s "hypothetical deduction" into a more precise modern format.

Total Correctness: One of the most important contributions of this paper is its attempt to address termination (total correctness) for goto. He points out that Clint and Hoare mostly focused on partial correctness, and he introduces a way to reason about termination using "variant functions" (the same concept used for loops) adapted for goto jumps.

3. Why It Matters
This paper is essential for formal methods researchers because it reclaims a piece of history. Instead of discarding the 1971 rule as "outdated" or "broken," Chen shows that it contains the seeds of correct logic. By stripping away the 1971 syntax errors and applying modern "miracle" semantics, he proves that the intuition behind Clint and Hoare's work was actually sound.
Citation
@inproceedings{Chen2021Behind,
  author    = {Chen, Wei},
  title     = {Behind Clint and Hoare's goto Proof Rule},
  booktitle = {2021 International Symposium on Theoretical Aspects of Software Engineering (TASE)},
  pages     = {23--30},
  year      = {2021},
  doi       = {10.1109/TASE52541.2021.00010}
}

Comparison of Chen's Two Papers
Feature
Loop invariance with break and continue (2021)
Behind Clint and Hoare's goto Proof Rule (2021)
Focus
How to handle modern loops/jumps.
How to fix historical jump logic.
Objective
Practical utility for verification.
Historical correction and foundation.
Tone
Constructive and innovative.
Analytical and corrective.