The automatic conversion of λ-expressions to combinator expressions simplifies mathematical proofs, but the combinator expressions are typically much larger and opaque as far as I can tell. The instrumented version of the interpreter reveals that several times as many steps are required to run a program when a substantial part has been converted to a combinator expression. The automatic expansion causes reused code to be duplicated. The conversion is much like in-lining. I suspect that this cannot be avoided. I think the expansion is exponential in the size of the input.

There is a peculiar sense in which the bare λ-calculus is like machine language. Just as a machine language subroutine must know the shape of its parameters, so must a λ-function know the shape of its input. In Scheme the shape can be tested with primitives such as pair?, number?, vector? and vector-length?: a list as argument can lead to different behavior than a number. In the pure λ-calculus every value is a function and all you can do with it is to invoke it. The simple ideas for car, cdr and cons require the recipient to know the list length. Imagine LISP without null? and nil or Scheme without null? and '(). I had not noticed that they were fundamental and not constructible. There is no way to find out about an argument except to invoke it. The invoker retains his integrity however. There is no synergy, I think. Strong statically typed languages ensure that the types are as the routine expects. Neither machine language nor the bare λ-calculus provide this protection.

Lest this be mis-understood, the λ-calculus, as interpreted by a program such as mine, is memory safe; it is merely that like machine language, a λ-program can not feel out its input as a Scheme program can sense that it has been fed a number. A machine language square root routine must take on faith that its input is a floating point number, but it can protect itself against bit patterns that are not valid floating point numbers.

With privileged mode, machine language can ensure integrity, and secrecy to portions of a software system that cohabit a machine with unknown code. With timer facilities headway of sorts can also be insured. At the cost of an interpretive mode languages, including the λ-calculus, can also do this too.

Opacity

There are short useful λ-expressions that I find opaque. I have followed the proof that the Y combinator provides recursion. It is not evident to me however from its short expression. I find more convincing that substituting the expansion of the definition of Y into (pr ((Y rd) 7)) gets the right answer.
Reference counting is tricky. Which abstraction level do we work at? Is it an actual expression value stored in RAM (well cache)? While computing an address I may compute another address which goes on a stack (soft or hard) that may get pushed onto a stack which is in RAM. Is this second address a reference that must be counted? Perhaps we can say that references on the stack need not be counted for they are surely ephemeral. There are other confusions.
Unify paragraph below with similar one above.

Imagine programming in Scheme without the type queries such as pair? number? string? symbol? boolean? vector?, even null?. I had not realized how fundamental these were to Scheme. Such primitives are somewhat like a machine instruction that would query data about its type. Some machines have provided this but today none do I think. Programs for today’s machines must know the types of data that they expect to find in memory or registers. The pure lambda calculus is like modern machines; the program must know what to expect. The naïve implementation of lists as a pair of the first element and the rest, founders for lack of a distinguished value to serve as the empty list. One must be able to test for emptiness and there is no value null?. Techniques used by Scheme interpreters to sense data types, using yet more data, are presumably necessary to do real computations in the pure lambda calculus. An interesting alternative is a compiler that does static typing and produces pure lambda code that knows the types of arguments. Even then it is typically infeasible to know the length of lists.