人们容易混淆语言实现保证

本文探讨了TLA+语义保证与模型检查器实现之间的差异，解释了为什么初学者在使用PrintT等副作用操作符时会遇到困惑，以及这种抽象泄漏如何影响编程体验。