Basically, proof theory is concerned almost exclusively with the study of formal proofs, and its principle tasks ca be summarized as follows.
When we say “a programming language is safe”, we are typically saying that the language is strongly typed and can capture errors through its robust type system. A type system is a very good example of proof system because we have a set of axioms and a system of logic–typing rules. Thus we can extract many useful information under this system and build a relationship between this proof system and another logic system (e.g., the runtime evaluation rules of the program). A program is well-typed means that the runtime behavior will never go wrong.