(Untitled)

Such a synthesis is offered by the principle of Propositions as Types, which links logic to computation.

Philip Wadler, “Propositions as Types”