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.

FROM:

Strange Loop Conference

'Propositions as Types' by Philip Wadler

Source

The program is a path to solving a proof - to proving a statement correct or incorrect.