Thanks for the attempt to explain. However, it's slightly off on several fronts, so I'd like to set the record straight. I don't know what you mean when you s

Thanks for the attempt to explain. However, it's slightly off on several fronts, so I'd like to set the record straight. I don't know what you mean when you say it's not a "traditional mathematical definition". It's both traditional and mathematical enough. An "operational semantics" is not necessarily a simplification. Whether or not it's a simplification is a function of what you are specifying. We chose a route whereby a compiler reduces all of JS to a simpler language (λJS) and then provided an operational semantics for that simpler language. Neither is this non-mathematical nor is the simplification inherent to an operational semantics. Your restatement of soundness contains dangerous words that have other, technical meanings (like "valid") and is also not quite right. The soundness being proven here is called "untyped soundness", and it simply means "the semantics didn't forget any cases that should have been defined". Perhaps that is what you meant to say, but I'd suggest this way of saying it is a lot less obscure. Our previous formulation missed a few cases. The cases were sufficiently obscure that all our prior testing and use did not catch them. So I'd say this hardly warrants the label "severe". You can see the sum total of change here (the link was in the original post): https://github.com/brownplt/LambdaJS/commit/9a7e67ab896c8db3f12cdfe3aa6fe74e192b1b00 https://github.com/brownplt/LambdaJS/commit/9a7e67ab896c8db3... Also, our previous attempt to confirm untyped soundness was not hand-written. It too was mechanical, but it used a state-exploration strategy. This caught lots of problems, which we fixed, but because it could not explore the state exhaustively, it missed a few that we hadn't noticed. The strategy in this post explores the state exhaustively (through a proof-assistant). Hope that clarifies.