| See the Curry Howard Correspondence: https://en.wikipedia.org/wiki/Curry%E2%80%93Howard_correspon... Essentially: all programming languages are logics, and all logics are programming languages; all programs are proofs, and all proofs are programs; all (static) types are propositions, and all propositions are (static) types; and so on for every facet of computer programming and theorem proving. It's usually pointless to apply this to existing languages/logics/etc., since they end up being pretty terrible. For example, in a dynamically typed language like Python there is only one static type; hence if we view it as a logic there is only a single proposition; all Python programs are proofs of that same proposition, including trivial programs like '42', and hence the logic is completely trivial. More sophisticated languages can still end up being pretty trivial. For example, in Java the value 'null' is a member of every type; hence from a logical perspective 'null' is a proof of every proposition. Hence Java also collapses into triviality (from the programming perspective: no matter how complicated we make our class hierarchy, or how long we make the dependency chains between our constructors, users of our API can just give 'null' for every argument and Java's type checker will gladly accept it) Even more 'hardcore' languages like Haskell, which don't have the 'null' problem (but do have a less-severe problem called "bottom", see http://chriswarbo.net/blog/2020-02-09-bottom.html ), end up being pretty trivial too. For example, Curry-Howard tells us that function types correspond to implication propositions, so 'T1 -> T2' is a function type with argument type T1 and return type T2, and also the proposition that T1 implies T2 (i.e. if T1 is true, then T2 is true). At first glance this looks really useful, e.g. we if we have a function with type 'CustomerRecord -> JSON' it's tempting to think of this as proof that CustomerRecords can be represented as JSON. Yet that's not what it says: in particular, the return type doesn't have any relationship to the input type. This function is actually stating that "if you give me any CustomerRecord, I can give you some JSON value". This is much less useful; e.g. we could implement this function by always returning the JSON value '"hello world"'. Hence the Curry Howard Correspondence only tends to be useful for languages which were designed to take advantage of it. Lean is one example; others are Agda, Coq and Idris. In all of these languages, proofs and programs are the same thing; functions and implications are the same thing; conjunctions and tuples are the same thing; and so on. This lets us prove propositions about programs, programatically generate proofs, and any combination of the two. Incidentally, the way that these languages avoid being trivial is by having dependent types. These let us state relationships between the input and output types of a function, like '(x: Int) -> Even (Double x)' ("if x has type Int, then doubling x is even"), or between the elements of a tuple, like '(x: Int, Even x)' ("a value x of type Int, and a proof that x is even"). I wrote a bit about this at http://chriswarbo.net/blog/2017-11-03-dependent_function_typ... The logic equivalent of a dependent function type is a universally quantified proposition (i.e. "for all x, ..."). The logic equivalent of a dependent tuple type is an existentially quantified proposition (i.e. "there exists an x such that..."). This tuple idea can also be extended to name/value records too. |