I know Dijkstra is famous for having said that we're mentally mutilated beyond hope of regeneration, but you know, I kinda think we didn't turn out half bad.
Practically everybody in my generation started off with BASIC. On the other hand, at some point (when?), this practice stopped, and the newer generations turned out fine starting out with more civilized languages.
https://homepages.cwi.nl/~storm/teaching/reader/Dijkstra68.p...
In original BASIC, the GOTO is a foundational mechanism and a majority of programs would have used it, sometimes extensively. Dijkstra thought for many reasons that this wasn't good style and didn't promote clear thinking. And yes, one consequence of that is that it would be harder to prove programs correct or just to reason about whether they were correct.
Programs that overuse GOTOs (or from the point of view of later structured programming and functional programming advocates, perhaps programs that use GOTOs at all) were stigmatized as "spaghetti code".
https://en.wikipedia.org/wiki/Spaghetti_code
By the way, this concern is not just about aesthetics: some of the ideas that Dijkstra was advocating are arguably those that newer programming languages like Haskell and Rust can use to find bugs in code automatically at compile-time, or to make it harder to write certain bugs at all. The line between Dijkstra's advocacy and these techniques is complicated but I think there is a connection. So partly we might say that Dijkstra was not just concerned with how to make it easier for humans to think clearly about program correctness, but ultimately also about how to make it easier for computers to help humans automatically determine (parts of) program correctness. And it's true that the GOTO style complicates that task.
Jeff Dunteman’s assembly programming books included a “chapter 0” that I always loved, and which really stuck with me for how creatively they taught those topics.
So I'm not convinced that even those who think they know how it works know it actually.