natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism = propositions as types +programs as proofs +relation type theory/category theory
In type theory a definition is the construction of a term of a certain type.
As such definitions are no different from proofs of theorems (due propositions-as-types). For instance the constructive proof that there exists a natural number consists of exhibiting one, and hence the definition of, say $2 \in \mathbb{N}$ is the same as a specific proof that $\exists x \in \mathbb{N}$.
definition/proof/program (proofs as programs)