Have terms (variabes and function application) atomic formula (including predicates) formulas (made up logically)
Curry-Howard Correspondance for predicate logic gives us dependent type theory.
Second order predicate logic gives types depending on terms and terms depending on types.