I assert here: “Neither machine language nor the bare λ-calculus provide this protection.”. The protection in question is memory safety that most modern computer languages give where the program is indeed oblivious to the underlying details of the real hardware in operation—the hardware is really abstracted. This is an obscure, difficult and important claim, I think, and thus worthy of expanded explanation.

When the λ-calculus replaces the hardware the program fragments must know the shape of the data that they work on. The (λ) program is not free to ask if an argument is a list, whether the list is empty, etc, just as a machine language program is not free to ask if a pointer is valid, unless a convention has been established, and followed such as ‘pointers with all zero bits designate nothing’. The several sites on the web that show how to build car, car, cons from λ-values do not provide the analog of pair? just as machine language programs do not provide a means for testing the contents of memory for being a floating point number or a word with a pair of addresses.

Consequently the program that would guarantee its behavior is at the mercy of other programs that build data for the former.

I think that something like a typed λ-calculus discipline would solve these problems if imposed on all ‘other programs’.

Comparing modern CPUs with the λ-calculus suggests that the λ-calculus lacks the analog of ‘privileged mode’ that modern CPU's have had since the 60’s. Both sorts of system are Turing complete, and secure systems can be built on either, but early CPUs and the λ-calculus seem to require an interpretive layer.