How is does type theory (coq, lean, agda), and logic programming (prolog, datalog) differ from each other.
Logic programming is a way of declarative specifying an algorithm, using classical 1st order logic and the implementation of the computation of that algorithm does not have to be specified.
Type theory is a way of declarative specifying an algorithm, using constructive logic, making program synthesis possible.