Programming languages for efficient computation It is impossible to write a programming language that allows all machines that halt on all inputs and no others. However, it seems to be easy to define such a programming language for any standard complexity class. In particular, we can define a language in which we can express all efficient computations and only efficient computations. 

For instance, for something like $P$: take your favorite programming language, and after you write your program (corresponding to Turing Machine $M'$), add three values to the header: an integer $c$, and integer $k$, and a default output $d$. When the program is compiled, output a Turing machine $M$ that given input $x$ of size $n$ runs $M&#39;$ on $x$ for $c n^k$ steps. If $M&#39;$ does not halt before the $c n^k$ steps are up, output the default output $d$. Unless I am mistaken, this programming languages will allow us to express all computations in $P$ and nothing more. However, this proposed language is inherently non-interesting.

My question: are there programming languages that capture subsets of computable functions (such as all efficiently computable function) in a non-trivial way? If there are not, is there a reason for this?
One language attempting to express only polynomial time computations is the soft lambda calculus. It's type system is rooted in linear logic. A recent thesis addresses polynomial time calculi, and provides a good summary of recent developments based on this approach. Martin Hofmann has been working on the topic for quite some time. An older list of relevant papers can be found here; Many of his papers's continue in this direction.

Other work takes the approach of verifying that the program uses a certain amount of resources, using Dependent Types or Typed Assembly Language.

Yet other approaches are based on resource bounded formal calculi, such as variants of the ambient calculus.

These approaches have the property that well-typed programs satisfy some pre-specified resource bounds. The resource bound could be time or space, and generally can depend upon the size of the inputs.

Early work in this area is on strongly normalising calculi, meaning that all well-typed programs halt. System F, aka the polymorphic lambda calculus, is strongly normalising.  It has no fixed point operator, but is nonetheless quite expressive, though I don't think it is known what complexity class it corresponds to. By definition, any strongly normalising calculus expresses some class of terminating computations.

The programming language Charity is a quite expressive functional language that halts on all inputs. I don't know what complexity class it can expression, but the Ackermann function can be written in Charity.