# Types are propositions, functions are proofs

In a pure functional languages based on substitution, such as Simply Typed Lambda Calculus, various systems of various Logic, or high level languages like Miranda or Haskell, types could be viewed as propositions, while semantically correct pure functions (without side effects) define (or implement) actual proofs.

Each sub-expression inside a pure function (which as a whole is one single expression) has its own type.

Nested functions corresponds to a program, which is a single expression too. (The result of evaluation of `main :: IO ()` in Haskell is an expression to be evaluated (reduced to a value) by the runtime.

The proof of an implication `B → A` is a function, which takes a proof of the antecedent `B` (a value from a nested function) into a proof of the consequent `A`. This.

The function that proves `B → A` is applied to the proof of `B` to yield a proof of `A` (which is a value).

Introduction + elimination (reduction) is a transition - a step further, preserving the `Truth`.

This is the formal logic.

The reduction rule for functions applies when a `lambda` term introduces a function, which is immediately eliminated by an application (`apply`).

Similarly, the reduction rules for `Pair`s apply when a constructor `CONS` introduces a `Pair`, which is immediately eliminated by a selector `CAR` or `CDR`.

There is nothing extra to it.

Start from the types, and the terms and reductions follow. The terms follow as introducers (`define` and eliminators `apply` for the type, and the reductions follow when an introducer meets an eliminator (inside `eval` which calls `apply`), and type safety follows by showing that each of the reduction rules preserves type derivations, which means the whole thing is consistent (without any contradiction).

This is what is called well-typed, type-sage or fp-complete - consistency guarantee.

Provided that semantics of each function (or proof) are correct, the whole program, then, is correct. The way some Math or Logic is correct.