Lambda Calculus is a formal language to define computations. In Lambda Calculus any computation is defined in terms of evaluation of Lambda Abstractions - application of procedures. Evaluation is defined as substitution of terms.
The fundamental, unique property is that the order of evaluation (substitution) does not matter as long as procedures are pure functions (same input - same output. Always) and referential transparency is maintained.
The Substitution Model
In Math, which is the science of abstract patterns, only
equal quantities (the same entity) could be substituted for an equal (same).
Each occurrence of a Number 2 is a reference to the same unique concept (abstract entity) of a Number 2.
In Nature, in What Is, only
equivalent could be substituted to equivalent. Two hydrogen atoms (or two water molecules) are not the same, but they are equivalent. Two water molecules have the same structure, but this very notion of sameness is an abstraction of the mind. Structures are equivalent.
In programming Equivalence is defined by behavioral traits using Duck Typing (if it walks like duck and quacks like a duck). The key abstractions are Interfaces (a set of function signatures) and Protocols (a set of named if-then-else rules).
Assert what is equal (or equivalent).
Good programming languages provide means to model (using protocols and interfaces) the domain of a program and to define embedded DSLs for subdomains. DSLs usually from a hierarchy of layers.
Erlang could be considered as an implementation of Untyped Lambda Calculus.