let as used in programming languages is defined in lambda calculus as per https://en.wikipedia.org/wiki/Let_expression#Let_definition_defined_from_lambda_calculus
The simple, non recursive let expression was defined as being syntactic sugar for the lambda abstraction applied to a term. In that definition,
$$ ( let_s \quad x = y \quad in \quad z ) ≡ ( λ x . z ) y $$
let also has another definition in terms of logic, per
In mathematics the let expression is described as the conjunction of expressions. In functional languages the let expression is also used to limit scope. In mathematics scope is described by quantifiers. The let expression is a conjunction within an existential quantifier.
$$ ( ∃ x E ∧ F ) ⟺ let \quad x : E \quad in \quad F $$
where $E$ and $F$ are of type Boolean.
The let expression allows the substitution to be applied to another expression. This substitution may be applied within a restricted scope, to a sub expression.
In the definition $ ∃ x E ∧ F $ by logic,
- Are $E$ and $F$ both propositions?
what does $ ∃ x E ∧ F $ mean? Does it mean $ ( ∃ x E) ∧ F$ or $ ∃ x (E ∧ F )$?
what "substitution" does $ ∃ x E ∧ F $ allow?
how does $ ∃ x E ∧ F $ relate to the first definition $( λ x . z ) y$ ?
Does language C have similar construct to