Theories of enormous computational and proof-theoretic strength have been developed by the computing science community for the purpose of obtaining some form of expressive power. The second order lambda calculus and the theory of constructions, together with its various extensions, are obvious examples. In this paper we challenge this design strategy from the perspective of constructive functional programming. Our aim is to show that very weak theories suffice for this activity. More positively, our motivation is to develop theories which are a more accurate reflection of computational practice.