I had not looked at the Promising Semantics paper of 2017. Thank you for the reference. That said, what I have learned from watching this space for a decade is

I had not looked at the Promising Semantics paper of 2017. Thank you for the reference. That said, what I have learned from watching this space for a decade is that even formal proofs are no match for the complexity of this general problem. You have to get the definitions right, you have to prove the right statements, and so on. There is still plenty of room for error. And even a correct, verified proof is not really an insight as to why things work. Experts were telling us in 2009 that OOTA had been resolved to everyone's satisfaction, only to discover that it wasn't, really. Maybe Promising Semantics is the final answer, but maybe not. We need to get to the point where everything is obvious and easy to explain, and we're just not even close to that yet. Looking at citations of Promising Semantics in Google Scholar I found this Pomsets with Preconditions paper from OOPSLA 2020: https://dl.acm.org/doi/abs/10.1145/3428262 https://dl.acm.org/doi/abs/10.1145/3428262. It contains this sentence: "As confirmed by [Chakraborty and Vafeiadis 2018; Kang et al. 2018], the promising semantics [Kang et al. 2017] and related models [Chakraborty and Vafeiadis 2019; Jagadeesan et al. 2010; Manson et al. 2005] all allow OOTA behaviors of OOTA4." I take that to mean the jury still seems to be out on excluding all OOTA problems. Maybe the canonical example has been taken care of, but not other variants. And again we don't really understand it.