I think the crux of John’s point is that the paper was passed around the internet ten years ago (yes, yes, and before that too). It’s one of those things that people like to trot out to score internet points, and usually it’s clear that the person posting it hasn’t read it, or at least didn’t understand it. And then we all move on, so that next week somebody can post a link about using xor to make a linked list.
[Comment removed by author]
Because avoiding goto is easy. Formally verifying a program, especially one written in a dynamic imperative language with half its meaningful logic embedded in an extremely complex external system, is damn near impossible.