When language implementations add escape hatches or effectful operators that violate the language's formal semantics, developers get confused. Using TLA+ as the primary example, the post explores how TLC (the model checker) breaks TLA+'s guarantee of statement non-ordering: effectful operators like PrintT and Assert execute with side effects even when a guard clause would later discard the state, producing ghost outputs. The core issue is that these guarantee-breaking operators are syntactically indistinguishable from safe ones, unlike pragmas or preprocessors in compiled languages. The phenomenon generalizes to other declarative languages — Prolog cuts, backreferences in regex, ordered choice in grammars — wherever the operational model leaks through the declarative abstraction.
