  Proof theory has created new aims outside traditional mathematics,  especially in connection with computer science. Topics such as the  verification of correctness of computer programs are an outgrowth of  proof theory. Natural deduction has led to the Curry-Howard  correspondence and to connections with functional programming, and  sequent calculus is often used in systems of automatic proof search,  as in logic programming.