规范语言该不该带类型：Lean vs. TLA+
📝
内容提要
计算机科学家莱斯利·兰波特写论文说类型系统对数学有害，但他自己的规范语言TLA+却靠无类型集合论运转了二十多年。这个事实让一群用Lean证明定理的数学家很不服气，两边吵了快三十年还没停。 ## 规范语言和形式验证 规范语言是一门不跑程序的编程语言。它只负责描述系统该做什么，不负责让机器执行。工程师用规范语言写下“这个数据库永远不能丢数据”，然后交给工具去查有没有漏洞。它和Java、Py
