# Proofs techniques related to Curry–Howard correspondence

I am looking for sources about formalized notion of programs. This seems to be closely related to Curry-Howard correspondence, but one could also track this back to Universal Turing Machines and its ability to read description and input of any TM.

When reading about Curry-Howard correspondece I feel that the primordiality of UTM-s can harm research on programs with the unique conclusion that any program can be reduced to symbols, states and rules. Does there exist the opposite approach, where high-level computation systems are defined and examined? What are good resources about it?

• A good starting point would be Hoare Logic. – Dave Clarke Aug 9 '12 at 6:45
• You forgot Lambek, if you included him in the list then you'd have all of category theory at your service. – Artem Kaznatcheev Aug 12 '12 at 2:43

What you want exists, and is an enormous area of research: it's the entire theory of programming languages.

Loosely speaking, you can view computation in two ways. You can think of machines, or you can think of languages.

A machine is basically some kind of finite control augmented with some (possibly unbounded) memory. This is why introductory TOC classes go from finite automata to pushdown automata to Turing machines --- each class takes a finite control and adds some more memory to it. (Nowadays, the finite control is often limited even more, as in circuit models.) The essential thing is that the finite control is given up front, and all at once.

A language is a way of specifying a whole family of controls, in a compositional way. You have primitive forms for basic controls, and operators for building up larger controls from smaller ones. The primordial language, the lambda-calculus, in fact specifies nothing but control -- the only things you can define are function abstractions, applications, and variable references.

You can go back and forth between these two views: the $snm$-theorem is essentially a proof that Turing machines can implement function abstraction and application, and Church encodings demonstrate that the lambda-calculus can encode data. But there's nontrivial content in both of these theorems, and so you should not make the mistake of thinking that the two ways of understanding computation are the same.

Researchers in complexity and algorithms typically take machines as fundamental, because they are interested in costs and in feasibility results. To exaggerate a bit, the basic research question they have is:

What is the least powerful machine that can solve a certain kind of problem?

Language researchers take languages as fundamental, because we are interested in expressiveness and impossibility results. With a similar exaggeration, our basic research question is:

What is the most expressive language that rules out a certain kind of bad behavior?

As an aside, note how the two goods each kind of theoretician values are directly in conflict! Good work in algorithms and complexity lets you solve a harder problem, using less resources. Good work in languages lets programmers do more things, while forbidding more bad behaviors. (This conflict is basically why research is hard.)

Now, you might ask why more Theory A types don't use languages, or why more Theory B researchers don't use machines. The reason arises from the shape of the basic research question.

Note that the stylized basic research question in algorithms/complexity is a lower bound question -- you want to know that you have the best solution, and that there is no possible way to do better, no matter how clever you are. A language definition fixes the means of program composition, and so if you prove that a lower bound with a language model, then you might be left with the question of whether it might not somehow be possible to do better if you extended your language with some new feature. A machine model gives you the whole control in one go, and so you know everything the machine can possibly do right from the outset.

But machine specifications are exactly the wrong thing for saying interesting things about blocking bad behavior. A machine gives you a whole control up-front, but knowing that one particular program is okay or bad doesn't help you when you want to extend it or use it as a subroutine -- as Perlis's epigram states, "Every program is a part of some other program and rarely fits." Since language researchers are interested in saying things about whole classes of programs, languages are much better suited for purpose.

• This is similar to my view that algorithms folks are really doing applied complexity theory, not programming :). Excellent answer. Also, in practice complexity folks can't prove lower bounds for generic machines, and end up restricting to a weaker expressive model (i.e a kind of language) – Suresh Venkat Aug 9 '12 at 13:07
• Very helpful answer. I noticed that it is possible to define control alone (lambda calculus). Next, smn theorem gives lambda calculus implicit capability of encoding data. It also gives high level control (function abstraction & application) to Turing machines – which as I assume can explicitly encode data and basic control (apparently this is stated in the third paragraph about machines). – AllCoder Aug 9 '12 at 19:40