当语言实现破坏语言保证时人们为何感到困惑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+ 语义中语句的顺序无关紧要，交换两个赋值语句不会改变输出结果。这种语言设计真的很巧妙！这意味着基本上不存在步内竞态条件——一个函数可以更新某个变量而不影响其他函数如何使用它。

好了，现在初学者不可避免地会遇到一个问题：

\* 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 这样的具效果操作符。这可能导致守卫语句出现问题。从理论上讲，这两个脚本块是等价的：

/\ 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）本意就是作为逃生舱口。所以如果你需要使用它们，说明你已经在做一些相当奇怪的事情，这就更加令人困惑了。

更糟糕的是，没有任何语法或视觉上的区别能区分破坏保证的 TLC 操作符和常规安全的 TLA+ 操作符。在编译型语言中有 pragmas 和预处理器，可以让编译器做一些语言本身做不到的事。但这些通常具有明显不同的语法形式，让你一眼就知道这里有危险。

这让我想起 Neel Krishnaswami 那篇令人惊叹的文章《什么是声明式语言》：

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

使用截断（cut）的谓词在语法上具有视觉上的明显区别，但一个使用了截断的谓词在外观上与逻辑上纯净的谓词并无二致。不过，这比我们在 TLA+ 中遇到的问题要稍微简单一些，因为截断仍然是语言语义的一部分。

（话虽如此，不同的 Prolog 方言在打印字符串的方式上各不相同，这些操作会给 Prolog 带来副作用，而且它们与其他谓词在外观上也无法区分。所以同样是这个问题！）

我实际上并没有解决这个问题的方案。我只是觉得这是一个关于抽象泄漏的有趣例子。也许我们可以编写一个代码高亮器，它能高亮所有间接使用了“奇怪”函数的函数之类的。