3 ms·
Excellent article, Reginald. 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
by gfaure 8y ago
Excellent article, Reginald.
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?
- braythwayt 8y agoThis is the best comment! 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.