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 computer science a program is a construction of a term of a certain type (the output of the program).
Under computational trinitarianism this is essentially the same as a proof in type theory of the proposition presented by the type (see at propositions as types and proofs as programs).
definition/proof/program (proofs as programs)