Church encoding is not a good way to write real-world programs. There, I said it. I said it was useful theory. E.g. a way to shrink a programming language to r

Church encoding is not a good way to write real-world programs. There, I said it. I said it was useful theory. E.g. a way to shrink a programming language to remove data types so there's less drudgery in proofs about that language. That's not a regular programming task in the slightest.