Propositions in logic correspond to types in a programming language.
Proofs in the logic correspond to terms and programs in the programming language
Simplification of proofs corresponds to evaluation of programs.
Strange Loop Conference'Propositions as Types' by Philip Wadler
The program is a path to solving a proof - to proving a statement correct or incorrect.
Josh Beckman