言語実装の保証に人々は混乱する

TLA+の理論的な非順序保証と、モデルチェッカーTLCによる実装上の制約（PrintTなどの副作用演算子や変数定義順序の影響）の違いが混乱を招く。宣言的言語の抽象化が漏れ出る典型的な例であり、視覚的に区別できないことが問題を複雑にしている。