Proof-Oriented Programming

“命题即类型”这一口号描述了数学命题和类型理论语言之间的对应关系。与此密切相关的是“作为程序的证明”这一概念，它本质上表明，为给定命题提供数学证明等同于编写一个程序，该程序将类型检查为等价类型(或者更确切地说，驻留该类型)。当然，这种能力根据所使用的类型系统的不同而有所不同；而足以表达整个高阶逻辑的类型系统称为依赖类型系统。非正式地说，这样的系统是特别的，因为它们允许我们谈论几乎任何事情，允许用户谈论任意的数学问题，或者关于代码的性质。

The slogan "propositions as types" describes a correspondence between mathematical propositions and the language of type theory. Closely related is the notion of "proofs as programs", which essentially states that providing a mathematical proof for a given proposition is equivalent to writing a program that type-checks as the equivalent type (or rather, inhabits that type). This power, of course, varies based on the type system used; and type systems that are powerful enough to express the entirety of higher-order logic are known as dependent type systems. Informally, such systems are special because they allow us to talk about almost anything, allowing users to talk about arbitrary problems of mathematics, or properties about code.