当语言实现违背语言承诺时，人们会感到困惑People get confused when language implementations break language guarantees

请看下面的 Python 程序：

# x = 1, y = 2
x = 0
y = x
print([x, y])

它会输出 [0, 0]。如果我们交换这两个赋值语句的顺序，输出就会变成 [0, 1]。每个赋值操作都发生在独立的时间步中。几乎所有命令式语言都是这样工作的。

现在请看下面的 TLA+ 代码片段：

\* x = 1, y = 2
/\ x' = 0
/\ y' = x
/\ PrintT(<<x', y'>>)

它会输出 <<0, 1>>。与命令式语言不同，TLA+ 将“更新”和“时间步”的概念分离开来。我们读取 x' = 0 时，意思是“在下一个状态中，x 将是 0，但在当前状态中它仍保持原值”。因此在每个状态中，x 和 x' 本质上是相互独立的变量。正因如此，TLA+ 的语义中语句的顺序无关紧要，交换两个赋值语句不会改变输出结果。这门语言的设计确实很巧妙！这意味着基本上不存在状态内的竞态条件。一个函数可以更新某个变量，而不会影响其他函数对该变量的使用。

好了，现在初学者 inevitably 会遇到这样一个问题：

\* x = 1, y = 2
/\ x' = y'
/\ y' = x
/\ PrintT(<<x', y'>>)

这段代码会崩溃，因为 y' 尚未定义。但如果我们交换这两个赋值语句的顺序，它就能正常运行并输出 <<1, 1>>。所以显然前面说的“顺序无关”完全是一派胡言。

其实并非如此。TLA+ 的语义仍然保证顺序无关性。问题在于验证器并不能完美实现 TLA+ 的语义。y' > 0 是一个完全合理的“赋值”，但它对应无限多个可能的下一个状态！因此主模型检查器（TLC）要求 y' = some_value 必须在任何其他使用 y' 的地方之前出现，这就导致顺序现在变得重要了。

更大的问题出在 PrintT 上。TLA+ 的语义之所以能保证顺序无关，是因为其语义本身不允许副作用。而模型检查器引入了具有副作用的操作符，如 PrintT、Assert 和 IOExec。这可能会在守卫语句中引发问题。理论上讲，下面这两个代码块是等价的：

/\ x = 0 \* guard statement
/\ P()
/\ x' = x + 1

/\ x' = x + 1
/\ P()
/\ x = 0 \* guard statement

当 x = 1 时，由于守卫子句的存在，这两个代码块都不会进入新状态。但模型检查器会逐行求值，这意味着在第二个代码块中，它会先执行 x' = x + 1 和 P()，然后才遇到 x = 0 并丢弃该状态。如果 P 是一个标准的 TLA+ 操作符，这没有问题；但如果它是 PrintT 或 Assert，就会先产生副作用，导致出现一些奇怪的“幽灵”输出，这些输出并不对应任何实际的下一个状态。

“TLA+ 语义所保证的内容”与“TLC 具体实现方式可能破坏这些保证”之间的这种差异，是让人困惑的巨大根源！更糟糕的是，像 IOExec 和 TLCSet 这类操作符本应作为应急出口（escape hatches）使用。所以如果你需要用到它们，说明你已经在做一些相当奇怪的事情，而这只会让情况更加令人困惑。

更雪上加霜的是，在语法或视觉上根本无法区分那些会破坏保证的 TLC 操作符和常规安全的 TLA+ 操作符。在编译型语言中，你有编译指示（pragmas）和预处理器，它们允许编译器做语言本身做不到的事情。但这些通常具有 visually distinct 的语法，所以你一眼就能看出这里有“龙”（危险）。

这让我想起了 Neel Krishnaswami 那篇精彩的文章《What Declarative Languages Are》：

这也让我们可以做出一个预测：任何声明式语言中最不受欢迎的特性，一定是那些暴露操作模型、破坏声明式语义的特性。因此我们可以预测，人们会讨厌（a）正则表达式中的反向引用，（b）文法中的有序选择，（c）查询语言中的行 ID，（d）Prolog 中的 cut，（e）约束语言中的约束优先级。

Prolog 中的 cut 具有视觉上独特的语法，但使用 cut 的谓词在视觉上与逻辑上纯粹的谓词并无区别。不过，这比 TLA+ 中的情况稍微简单一些，因为 cut 仍然是语言语义的一部分。

（话又说回来，不同的 Prolog 方言打印字符串的方式各不相同，这会给 Prolog 带来副作用，而这些副作用在视觉上也无法与其他谓词区分开来。所以问题本质相同！）

我其实并没有解决这个问题的办法。我只是觉得这是一个非常有趣的“抽象泄漏”的例子。也许我们可以写一个代码高亮工具，把所有间接使用了“奇怪”函数的地方都高亮出来，或者做点类似的事情。