Okay, I'll try to be charitable with you here and assume you've just missed this.
The problem with claims like:
> Nock is not practical. He is certainly not maximizing practicality by making a combinatory logic that can only increment integers and then recognizing and "accelerating" a particular implementation of decrement!
Is that you are evaluating a component of a larger system in isolation. The form of your argument is that this component, which is a language, has obvious deficiencies/impracticalities that can be established in terms of the language itself and how it relates to other languages.
But this doesn't take into account how the language (which is the component I spoke of) relates to the system in which it's embedded.
The appearance of impracticality is often present in foundational systems. How easy would it be do use your same form of argument and deride the Peano axioms as obviously impractical because: look how much work it is to do arithmetic with a 'successor function'—ridiculous! (i.e. the 'impracticality' depends completely on what you're trying to do with it)
This was what I was trying to investigate from the beginning: how have you verified that Nock's peculiarities don't have legitimate reasons in the context of the system of which it is a component?
If you review our conversation, you'll see that's what I was trying to figure out since my very first statement—and to this point, you have still not addressed it.
The initial poster is likely weary. I’ll try my hand exactly once. I know it can be frustrating for both parties, because sadly, to know that an expert is right, you need a bit of expertise.
Here we go.
Symmetries are useful to understand a domain. If you have one, you know that a point on the left will appear on the right. So question like “but how do you know that there really is a point on the right?” is simply because you know the proof of symmetry.
The answer to “how have you verified that Nock's peculiarities don't have legitimate reasons in the context of the system of which it is a component?” is in the same way. They mention Curry-Howard correspondence: I don’t want to lose too much time on it, but yes, it is a symmetry, so the point on the left called Nock has a corresponding point on the right called lambda calculus with the same properties; and the claims made by Nock’s author about there being no symmetry are disproved by old proofs.
In fact, there are a lot of 50-year-old systems that fulfill Nock’s goals. Since it is an old field, the majority of them had time to develop into practical systems that are much, much clearer and less esoteric.
Which brings me to the goal of Nock. Why do something esoteric when a bit of field knowledge shows the complexity is unwarranted?
One possibility is NIH.
A more likely explanation is getting users into the sunk cost fallacy. Why more likely? Because this technique has been used repeatedly by the author in other fields, like his political essays. I am not the first to have that thought; a quick Google search brings this: https://www.lesswrong.com/posts/6qPextf9KyWLFJ53j/why-is-men...
It does work. So many pixels spilt over an awkward language named after a famous anti-semite admired by the author, Albert Jay Nock.
Hi espadrine. I appreciate your well-intentioned comment, but I believe the issue here is not about grasping the symmetry argument, rather it's that the symmetry argument is not an answer to the the actual question I've been posing since the beginning.
Please correct me if I'm wrong—but the symmetry argument is basically: Nock could be classified as a concatenative combinatory logic, which is a variation of "classical" combinatory logic; this classical variation, or a particular incarnation like the SKI combinator calculus, can be viewed as a variation on the untyped lambda calculus.
That establishes an association between Nock, the alternative posted by xkapastel (which is a concatenative combinatory logic), and the lambda calculus.
So from here we can say, "why not just use the non-obscure bit of combinatory logic instead?" (we choose this over lambda calculus since Nock's approach appears concentative too, avoiding lambdas)
And my answer is that if all you need is a concatenative universal model of computation—then you're done!
But—where is it actually established that that is the only requirement for Nock in the context of Urbit? That is the question I've been asking the whole time, and which is not answered by the symmetry argument.
Nock's essential structure may be that of a concatenative combinatory logic, but that doesn't mean there aren't other aspects of its design which are important for how it relates to other particulars of the Urbit system (for instance: maybe this variation has nice performance properties in connection with other parts of Urbit—I don't know).
The problem with claims like:
> Nock is not practical. He is certainly not maximizing practicality by making a combinatory logic that can only increment integers and then recognizing and "accelerating" a particular implementation of decrement!
Is that you are evaluating a component of a larger system in isolation. The form of your argument is that this component, which is a language, has obvious deficiencies/impracticalities that can be established in terms of the language itself and how it relates to other languages.
But this doesn't take into account how the language (which is the component I spoke of) relates to the system in which it's embedded.
The appearance of impracticality is often present in foundational systems. How easy would it be do use your same form of argument and deride the Peano axioms as obviously impractical because: look how much work it is to do arithmetic with a 'successor function'—ridiculous! (i.e. the 'impracticality' depends completely on what you're trying to do with it)
This was what I was trying to investigate from the beginning: how have you verified that Nock's peculiarities don't have legitimate reasons in the context of the system of which it is a component?
If you review our conversation, you'll see that's what I was trying to figure out since my very first statement—and to this point, you have still not addressed it.