That is exactly right; an excellent interpretation of Dijkstra's paper and Dominus's analysis! Any block that has more than one entry (this doesn't happen quite as often), or more than one exit (this happens a lot) will be difficult to come up with a formal proof. And this is why last, next, etc., can be seen as "limited semantic" forms of goto.
As I think it over, I can't come up with any good explanation of where we might jump into code blocks at multiple entry points. An exception might be a given/when block. If fall-through is used, then the block has multiple entry points. And if fall-through isn't used, it has multiple entry and exit points. But on the other hand, given/when can be compared to a chain of if-else blocks, so in that sense perhaps the notion of multiple entry/exit points may sort of break down.
So where do we have an example of common coding practices that involve multiple entry points?