- 像Python这样的命令式语言按时间顺序逐步执行赋值，而TLA+将更新与时间步骤分离，使其语义中顺序无关。
- TLA+初学者在使用未定义的变量（例如赋值前的y'）时会遇到问题，因为TLC等验证器要求赋值有特定顺序，打破了非顺序保证。
- TLC中具有副作用的运算符（如PrintT、Assert和IOExec）违反了TLA+的无副作用语义，在守卫条件失败时会导致幽灵输出等意外效果。
- 安全的TLA+运算符与TLC的逃生门之间没有视觉区别，导致混淆，类似于Prolog的cut或其他声明式语言中暴露的操作特性。
- 这段文本引用了Neel Krishnaswami的观察：声明式语言中最不受欢迎的特性往往是那些通过暴露操作细节而破坏声明式语义的特性。