I think it would be interesting to see the operational semantics for a very small subset of the language. Applying that type of formalism would likely suss out or highlight the corner cases like the ones highlighted in the article.