So we have to understand that our object of concern is the following ratio: A is a specification and the a is a program meeting the specification A. The kind of relationship running between these two notions is precisely the same kind of relationship running between these two notions, that is A is a theorem or a proposition and a is a proof of A. So this equality essentially says that a very fruitful way of considering programs is to view them as proofs of theorems. And indeed it is the case that any proof of any theorem in a formal system has indeed a computation content. And we will see in this course how such a computation content can be described and eventually extracted. But here in order to deepen our analogy here are a list of other similar ratio. A is a problem or a task and a is a method for solving A. Or capital A is an intention or an expectation and a is a method for fulfilling or realising capital A.
Finally, in the context of l calculus here is how our conceptual analogy can be phrased: A is a type and a is l term of type A. Furthermore, normalisation of a proof or a l term corresponds to evaluation of a program. So indeed here would have a three-layered ratio. A this is not just a metaphoric language. All these correspondences can be cast into a formal way and this will also be seen in this course. So we can summarise this by saying that functional languages can also be viewed as languages for proofs.
