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.