In reply to @toonn:matrix.org
Yes. Though I'm not saying that is the only difference.

In reply to @stablejoy:matrix.org
Oh I see now, its like describing two directions. The assignment is describing direction from value to variable and the binding from identifier to value?

Also, sorry it's long, but in terms of basic lambda calculus thingies you don't get to have named functions or values at all, all you have is 1) functions that accept values (1 value to be precise) and that value being applied into the body of that function (that is the input value is substituted for the name inside the body as-is and the "head" of the function is plucked off, e.g. in λx.x λx is the head and . is a separator and x is the body and if you get something inside, you put it in λ__x__, it is piped through . and the inner x is replaced with the value you put inside the head, then head is removed and you are left with is the body!, also body can be xxx that would mean the input value is duplicated into three, so functions control WHERE you place something which directly affects in what order things are evaluated (applied to each other) later on which is key) 2) a rule is at the moment of evaluation (application) no free variable can be used for substitution, that is if you take something that does not represent anything concrete (has no actual value in its place) that value cannot be applied further into the body.

So because all you do is apply something from the head into the body, basically you view programs in pure languages as humongous onion functions that take some input and propagate it somewhere deeper modifying it in only god knows what ways, as the program evaluates, with every outer level of that huge onion removed, some inner layers gets a variable bound further and further until in the end you're left with some final value where everything that can be applied was applied.
In reality you're greatly abstracted away from the crazy logic of OG lambda calculus (and to some extent limited by practical computer design) with types like numbers strings and (I think) some operations on those types (you get typed lambda calculus), but the basic principles don't change.

What you see with named values (value being anything from a number to a function) is simply a programmer abstraction, you assign names to your values for pure convenience because in the end any such program can be rewritten without any names with only values as a bunch of functions and values nested inside each other, that is unlike the imperarive mindset where variables are used as storage spaces and not simply as names for values to be substituted

So again, yes, you bind names to values so that you can effectively as a programmer use those values in a short and concise way, not to actually store anything in them

Also, sorry it's long, but in terms of basic lambda calculus thingies you don't get to have named functions or values at all, all you have is 1) functions that accept values (1 value to be precise) and that value being applied into the body of that function (that is the input value is substituted for the name inside the body as-is and the "head" of the function is plucked off, e.g. in λx.x λx is the head and . is a separator and x is the body and if you get something inside, you put it in λx, it is piped through . and the inner x is replaced with the value you put inside the head, then head is removed and you are left with is the body!, also body can be xxx that would mean the input value is duplicated into three, so functions control WHERE you place something which directly affects in what order things are evaluated (applied to each other) later on which is key) 2) a rule is at the moment of evaluation (application) no free variable can be used for substitution, that is if you take something that does not represent anything concrete (has no actual value in its place) that value cannot be applied further into the body.

So because all you do is apply something from the head into the body, basically you view programs in pure languages as humongous onion functions that take some input and propagate it somewhere deeper modifying it in only god knows what ways, as the program evaluates, with every outer level of that huge onion removed, some inner layers gets a variable bound further and further until in the end you're left with some final value where everything that can be applied was applied.
In reality you're greatly abstracted away from the crazy logic of OG lambda calculus (and to some extent limited by practical computer design) with types like numbers strings and (I think) some operations on those types (you get typed lambda calculus), but the basic principles don't change.

What you see with named values (value being anything from a number to a function) is simply a programmer abstraction, you assign names to your values for pure convenience because in the end any such program can be rewritten without any names with only values as a bunch of functions and values nested inside each other, that is unlike the imperarive mindset where variables are used as storage spaces and not simply as names for values to be substituted

So again, yes, you bind names to values so that you can effectively as a programmer use those values in a short and concise way, not to actually store anything in them

Also, sorry it's long, but in terms of basic lambda calculus thingies you don't get to have named functions or values at all, all you have is 1) functions that accept values (1 value to be precise) and that value being applied into the body of that function (that is the input value is substituted for the name inside the body as-is and the "head" of the function is plucked off, e.g. in λx.x λx is the head and . is a separator and x is the body and if you get something inside, you put it in λx, it is piped through . and the inner x is replaced with the value you put inside the head, then head is removed and you are left with is the body!, also body can be xxx that would mean the input value is duplicated into three etc any combinations, so functions control WHERE you place something which directly affects in what order things are evaluated (applied to each other) later on which is key) 2) a rule is at the moment of evaluation (application) no free variable can be used for substitution, that is if you take something that does not represent anything concrete (has no actual value in its place) that value cannot be applied further into the body.

So because all you do is apply something from the head into the body, basically you view programs in pure languages as humongous onion functions that take some input and propagate it somewhere deeper modifying it in only god knows what ways, as the program evaluates, with every outer level of that huge onion removed, some inner layers gets a variable bound further and further until in the end you're left with some final value where everything that can be applied was applied.
In reality you're greatly abstracted away from the crazy logic of OG lambda calculus (and to some extent limited by practical computer design) with types like numbers strings and (I think) some operations on those types (you get typed lambda calculus), but the basic principles don't change.

What you see with named values (value being anything from a number to a function) is simply a programmer abstraction, you assign names to your values for pure convenience because in the end any such program can be rewritten without any names with only values as a bunch of functions and values nested inside each other, that is unlike the imperarive mindset where variables are used as storage spaces and not simply as names for values to be substituted

So again, yes, you bind names to values so that you can effectively as a programmer use those values in a short and concise way, not to actually store anything in them