Have you heard of the Curry-Howard correspondence [0]? This states that a type system is actually a logical system. The types are propositions (logical statemen

Have you heard of the Curry-Howard correspondence [0]? This states that a type system is actually a logical system. The types are propositions (logical statements) and their terms (the expressions of that type) are proofs. It's a straightforward syntactic correspondence: - A -> B (Function type) and A => B (Logical implication) - A * B (Product/Tuple type) and A /\ B (Logical conjunction) - A + B (Sum/Tagged union type) and A \/ B (Logical disjunction) Proving that A implies B is the same thing as writing a function that takes a proof of A and returns a proof of B. Proving the logical conjunction of A and B is the same thing as pairing together a proof of A and a proof of B. So writing a definition that has a certain type is the same thing as proving a theorem. Dependent types [1], which Coq, Agda, and Idris have, further the Curry-Howard correspondence. With dependent types, you can mention programs inside types and therefore express theorems about programs. You have: - The dependent function type (x : A) -> B(x), where the return type B(x) is a function of the input x. This is the same thing as universal quantification, "for all x of type A, B(x) holds." - The dependent tuple type (x : A) B(x), where the type of the second element is a function of the first element x. This is the same thing as existential quantification, "there exists an x of type A where B(x) holds." So with dependent types, you can write mathematical proofs about programs. For example, you can show that a binary operation is commutative. Another good example is the "vector" type [2], which is like the functional-style linked list type, but parameterized over a length. Thus, you can prove that an index out-of-bounds error cannot happen. If you want to learn more about the theory, keywords to search up are "constructive math/proof," "intuitionalistic logic," and "Martin-Lof/intuitionalistic type theory." [0] https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspondence https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon... [1] https://en.wikipedia.org/wiki/Dependent_type https://en.wikipedia.org/wiki/Dependent_type [2] https://github.com/idris-lang/Idris-dev/blob/master/libs/base/Data/Vect.idr https://github.com/idris-lang/Idris-dev/blob/master/libs/bas...