[stack] disallowing recursive definitions

Recently, I mentioned that if you disallow recursive definitions, then  
definitions can be thought of as macros or rewrite rules. In other  
words, you can replace every occurrence of foo in a program with foo's  
definition and then remove the definition without changing the meaning  
of the program. It is therefore trivial to remove all definitions in a  
program and be left with only a single function that only uses  
primitives built in to the system.

This dual view of definitions as functions and definitions as rewrite  
rules is, at least, aesthetically appealing. I began to think of what  
some other benefits of disallowing recursive definitions might be:

1. It isn't necessary to do tail call optimization; an appropriate  
combinator is used instead.
2. The type system and formalization of the language in general are  
simplified. A restriction on recursive definitions may actually be a  
requirement for a truly compositional type system.
3. WIth a small addition to the type system, it becomes possible to  
prove that the stack will not overflow given the correct set of  
recursive combinators. (Combinators like linrec would need to be  
disallowed or specially handled.)
4. Similarly, it becomes possible compute the maximum number of items  
that will ever be on the stack, and pre-allocate a stack of exactly  
the right size upon program initialization.
5. It allows additional ways of presenting code, such as an editor  
that can expand a definition inline to show what it does while still  
displaying a program with the same meaning.
6. It becomes possible to prove termination when using recursive  
combinators that always terminate given that their arguments always  
terminate (such as primrec).

There are likely other benefits that I'm missing.

The question therefore is how critical recursive definitions actually  
are. They're not necessary in an absolute sense; any recursive  
function can be expressed using while. Essentially, it seems like  
disallowing recursive definitions has the same sort of tradeoff as  
disallowing multiple references to the same value (and therefore  
enforcing linearity): Many nice properties emerge and things are  
simplified, but it may simply be too much of a pain. I think it may be  
worth a shot.

Thoughts?

- John