Wadler写了一篇令人惊叹的论文：Propositions as Types - 他在其中谈到了Howard-Curry对应关系，您可以根据程序类型检查程序行为。（对于给定的语言子集）。
最近Rich Hickey发布了Clojure 规范，用于定义数据和函数规范。
评论员在这里写道：
从 Wadler 我们有 props ≅ types, specs ≅ props -> types ergo 可以进行静态规范/合同/类型检查。
我的问题是：Clojure 的规范是否等同于 Wadler 的提议？
Propositions as Types 专门讨论了自然演绎和简单类型 Lambda 演算 (STLC) 之间存在的同构，这两种形式分别适用于逻辑和编程语言。这意味着当您在 STLC 中编程时，您可以将您的程序转换为逻辑命题。
例如，这些是等价的：
(a -> b) -> a -> b
P implies Q
P
therefore Q
第一个是函数的类型签名，第二个是逻辑命题。现在，当您“Clojure 的规范是否等同于 Wadler 的主张？” 您要问的是“我们可以将 Clojure 规范转换为逻辑语句吗？” 或者由于同构，“我们可以将 clojure 规范转换为 STLC 吗？”
规范允许我们使用任何和所有 Clojure谓词。这使得规范非常灵活，但它也是看到规范不是命题的关键。
使 STLC 作为逻辑工作的关键特征之一是所有项都归约，或者换句话说，STLC 中的所有程序都终止。Clojure 没有这个属性，很容易编写永远不会终止的 Clojure 程序。为了使任何编程语言成为一致的逻辑，它必须具有这种终止属性，因为“不终止”等同于逻辑上的矛盾。由于规范可以使用任何 Clojure 函数，因此您可以编写一个不会终止的规范，因此不能转换为 STLC。所以 Clojure 规范并不等同于 Wadler 的主张。
正如Clojure 规范的文档所述，规范不是类型系统。规格不关心证明，但类型是。类型将我们可以编写的程序限制为可以静态证明“正确”的程序。类型系统具有不同级别的功能和表现力，但健全的类型系统证明了您的代码的某些属性。
规范并不能证明您的代码的属性，而是试图让您相信您的代码可以正常工作，并且在代码不正常时可以看到。规范不能静态运行，它们基本上是关于运行时值以及它们之间的关系。
但即使存在这些差异，类型和 Clojure 规范也服务于相似的实用目的，它们都让我们对代码更有信心，它们允许我们将语义编码到函数定义中，并且两者都可以帮助我们生成测试以帮助我们防止爬进我们的代码的错误。