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
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
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 (
Similarly, the reduction rules for
Pairs apply when a constructor
CONS introduces a
Pair, which is immediately eliminated by a selector
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.