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

<p>Loosely speaking, you can view computation in two ways. You can think of <em>machines</em>, or you can think of <em>languages</em>. </p>

<p>A <em>machine</em> 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. </p>

<p>A <em>language</em> 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 <em>nothing but</em> control -- the only things you can define are function abstractions, applications, and variable references. </p>

<p>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.</p>

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

<blockquote>
  <p>What is the <em>least powerful</em> machine that can <em>solve</em> a certain kind of problem? </p>
</blockquote>

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

<blockquote>
  <p>What is the <em>most expressive</em> language that <em>rules out</em> a certain kind of bad behavior?</p>
</blockquote>

<p>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.)</p>

<p>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. </p>

<p>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 <em>fixes the means of program composition</em>, 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 <em>gives you the whole control</em> in one go, and so you know everything the machine can possibly do right from the outset. </p>

<p>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 <em>one particular</em> 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 <em>classes</em> of programs, languages are much better suited for purpose. </p>

CC BY-SA 3.0
2012-08-09T13:07:29.100Z
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
CC BY-SA 3.0
2012-08-09T19:40:40.377Z
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
CC BY-SA 3.0
2012-08-09T08:35:30.563Z
2012-08-09T08:35:30.563Z
Neel Krishnaswami
<p>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.</p>

<p>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?</p>

CC BY-SA 3.0
2012-08-09T06:45:40.407Z
A good starting point would be Hoare Logic.
Dave Clarke
CC BY-SA 3.0
2012-08-12T02:43:14.973Z
[You forgot Lambek](http://www.haskell.org/haskellwiki/Curry-Howard-Lambek_correspondence), if you included him in the list then you'd have all of category theory at your service.
Artem Kaznatcheev
<pl.programming-languages><universal-computation><type-systems><program-verification><formal-methods>
Proofs techniques related to Curry–Howard correspondence
AllCoder
# Proofs techniques related to Curry–Howard correspondence

(Asked by: username_0 on 2012-08-09)

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?

**Tags:** pl.programming-languages, universal-computation, type-systems, program-verification, formal-methods
> **Comments:**
> **username_1**: A good starting point would be Hoare Logic.  
> **username_2**: [You forgot Lambek](http://www.haskell.org/haskellwiki/Curry-Howard-Lambek_correspondence), if you included him in the list then you'd have all of category theory at your service.  

---

## 1 answers

### Answer by username_3 on 2012-08-09. Score: 21 | Accepted answer

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.

> **Comments:**
> **username_4**: 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)  
> **username_0**: 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).  

---

