But all of this is only relevant if other peoples intuition is that a fair execution of the small program would indeed terminate.
This makes it a great demonstration of how people's intuitions are off! If a program will do "A or B" infinitely often, that doesn't guarantee it will do "A" even once. That implicit assumption, that "A could happen means A will happen", leads to a lot of bugs in production.
One of the reasons I'm so glad I learned TLA+ is because it completely reshaped how I think about time and programs. It cuts across the usual intuition and exposes where common sense breaks down.