�� ��Curry-Howard is the idea that static types are propositional formulas and expressions that have such types are their proofs. Under the Curry-Howard correspondence, a static typechecker analyzing your program is equivalent to a proof checker ensuring that your proof is valid.
People tend to invoke Curry-Howard to praise ML- and Haskell-style algebraic types (according to Curry-Howard, sum types are disjunction, product types are conjunction, and function/exponential types are implication).
Not entirely. There are type errors that are caught at compilation time.
A stark difference is that Lisp has the idea that type checking is done on values, not on symbols. If the compiler can deduce that a value is going to conflict in a given context, it will flag the error.
And types are checked at run time as well.