> Imagine a world in which logic, programming, and mathematics are unified, in which every proof corresponds to a program, every program to a mapping, every mapping to a proof!<p>For those of you that may not know, this is called the Curry-Howard(-Lambek) Correspondence[1]. It establishes an isomorphism between well-formed computer programs and formal logic. This isomorphism is fairly intuitive when doing something like (typed) λ-calculus, but it also applies to things like Java and C++.<p>[1] <a href="https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence" rel="nofollow">https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon...</a>