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

Source

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