Indeed, which is why I offered the pragmatic qualifier. It easily follows that the weakest precondition for L is that at least one of the weakest preconditions

Indeed, which is why I offered the pragmatic qualifier. It easily follows that the weakest precondition for L is that at least one of the weakest preconditions for every goto to that L holds. One can possibly do even better with some kind of flow analysis. The issue isn't that it's impossible, it's that programming is hard enough and it makes it much harder to be sure the code is correct. Or maybe put another way "not difficult" for Knuth and for the typical working programmer (or me) aren't identical. Thanks for sharing that paper! As an aside, it's really remarkable just how readable the state of the art papers such as the one you shared there from that era are. Either computing science has greatly advanced to the point where clarity is no longer achievable without years of specialized preparatory study or the quality of writing has regressed.