I followed it entirely with one exception: I can see that `maker(maker)` has the right type, but why is it the right value? How do we know, as we fill in the blanks, that this is the implementation that yields the right result?
I wondered this myself. I mean, I can test it and see that it appears to give the correct result, but how do I prove that it gives the correct result?
I didn't include it, but you can do reductions, successively replacing the names with their expansions, and you see that it works out was we want.
And in Combinatory Logic, there really is nothing else. If an expression has the correct "type," then it works. There's nothing except rearranging terms, duplicating terms, and erasing terms.
But that being said, I don't know if that's a "proof," and I especially don't claim that a proof about Combinatory Logic would say anything at all about JavaScript.
I followed it entirely with one exception: I can see that `maker(maker)` has the right type, but why is it the right value? How do we know, as we fill in the blanks, that this is the implementation that yields the right result?