As we have mentioned already, there is this very important analogy called Curry - Howard - Martin-Löf - De Bruijn analogy, which is an essentially announce to the following conceptual ratio.
A is a proposition, or A is a specification, or A is a problem or a task, or A is an intentional unexpectation, or A is a type, are all in the same relation respectively with a is a proof of A, in a constructive logic, a is a program meeting A, a is a method for solving the problem A, a is a method for realising the expectation A; a is a l term of type A.