Perhaps this is an artificial dichotomy? What we really want is verification that some properties hold. These properties should be specified in a uniform way, irrespective of the time that the check can apply.

When I specify a property, why do I have to also pick the time - 'run time' or 'compile time' and why the language used to specify exactly the same property is so different in each case? I think there is some unnecessary conflation here.

I dunno; I wouldn't use Church encoding in that situation. For the same reason I wouldn't use infinite precision rationals to represent 24bit R/G/B colours on a microcontroller, and I wouldn't use floats in a computer algebra system.

You seem to have strawmanned "functions are a perfectly good datastructure" into "always use functions for everything", which is (a) obviously not what I claimed and (b) not even the point I was trying to make; it was just a footnote pointing out that "code vs data" has nuances because sometimes our "data" is code.

> If you implement if-statements by passing two functions to a function which calls one or the other for truth and falsity, how do you determine dead code at compile time?

Supercompilation. Still, there's not much point taking something as expressive as functions, and using them to implement something impoverished and abstract like booleans. Much better to implement something actually relevant for your domain; for example, using functions to implement booleans, then using those booleans to implement permission checks (e.g. `if(isAdmin, doAction, permissionDenied)`), is harder and more complicated than just implementing the permissions checks directly using functions.

Note that this is something the actually happens all the time! Any time an OO programmer has two objects with different implementations of the same method (say, an `Admin` object whose `doAction` method does the action, and an `UnpriviledgedUser` class whose `doAction` method shows a "permission denied" message), they're essentially "implementing if-statements by passing two functions to a dynamic-dispatcher which calls one or the other for truth and falsity". It's not a problem.

Note that Smalltalk actually does implement "if statements" using objects with different `ifTrue` methods. Yet the only reason they do so, and in fact why any language has things as inherently-meaningless as booleans (and functions, strings, arrays, etc.), is because the language designers/implementers aren't able to predict the domains that we'll be dealing with. The best they can do is provide generic building blocks which are sufficiently expressive for us to construct semantically-meaningful domains for ourselves. Hence any attempt to implement <generic building block A> using <generic building block B> is usually pointless from a practical perspective (although is useful for learning): it's basically a constructive proof that <generic building block A> is expressive enough that we don't need <generic building block B> at all, and hence is self-defeating!

You said that using functions for everything was, and I quote, "perfectly good". That seems to imply to me that it cannot be improved, and conveyed an unwarranted absolute position.

Note that Smalltalk actually does implement "if statements"

Smalltalk is of course what I had in mind when I wrote that. And of course Smalltalk's lasting contribution is the dynamic optimization gymnastics it inspired to compensate for its design choices, and not the design choices themselves.

language designers/implementers aren't able to predict the domains that we'll be dealing with. The best they can do is provide generic building blocks which are sufficiently expressive for us to construct semantically-meaningful domains for ourselves

I'll deny this to my dying day. The most expressive language with the most generic primitives is not the best language, and it is far, very far from the best we language designers can do. The languages that give people the most ability to construct domains for themselves are the ones that end up with the lowest common denominators between codebases and programmers. It's the reason Lisp and Smalltalk didn't take over the world. Too much freedom is a bad thing; form is liberating, and more importantly, prosocial.

Example: "Someone in my building threw out a perfectly good audio amplifier. It just needed a blown fuse replaced inside! I hooked it up to some speakers and now using it for my TV."

It doesn't mean that the hardware is so advanced, it cannot be improved.

The "perfectly good" quote is accurate. I never said "for everything".