The claim that variable names are worthless is quite exotic in the general context. I value algebraically explicit operations as much as the next guy but I also write much better code when it's obvious to me what my code does, and good variable names are an important tool cognitively in that respect.
Yes, Tony's claim is a bit extreme, and I don't think it's standard practice in general. I just thought it was a nice counterpoint to the OP's claim.
Note, however, that this "do not needlessly name things" does show up in actual programming. In standard Haskell practice, it's common to write very short, abstract variable names whenever the function is general, and in turn you're encouraged to write general functions whenever possible.
Maybe it would be interesting to assert from a name a specific behavior or type. For example the test suite sees the variable name "description" and concludes that this should be a Unicode string and tests this automatically. A universal vocabulary could be agreed upon and automatically tested. Say lint for names.
I was thinking that names help in those areas where algebraically correct operations can still lead to broken domain logic. Type systems help verifying that a specified algebra functions coherently but they do not help in designing that algebra.
I.e velocity v, acceleration a are modeled as floats. To integrate from instance in time t0 to t1, v1 = v0 + (t1 - t0) * a.
Now, I can replace any of those arithmetic operators with other arithmetic operators and still the statement is algebraically correct. However, the calculation is probably wrong,e .g. v1 = v0 * (t1 / t0) - a is a such broken permutation.
Naming time at point 0 as t0 and at point 1 as t1 are helpful mnemonics that help here.
Sure, we can create data types (that contain floats) Acceleration, TimeBefore, TimeAfter, VelocityBefore and VelocityAfter and create function (since we are ignoring names) asdf->VelocityBefore->TimeBefore->TimeAfter->Acceleration->VelocityAfter but the rub is - the implementation of that function needs to do that floating point arithmetic at some point.
Wrapping it in an algebraically explicit container does nothing to help in the correctness of the computation in itself. The main benefit here is for the end user in form of explicit types. Here, the function signature proves the OP:s point - signatures can be enough to document a function. However, it does nothing to verify the implementation.
Floating point operations are inherently "dynamically typed" in the sense that from a semantic point of view only some operations make sense when forming equations but modeling all of these relations using a type hierarchy is really, really cumbersome - and after the type hierarchy is in place, the hierarchy itself cannot prove the equation is correct, it just sets it in stone. Maths in inherently dynamically typed and good names help write better equations. If anyone have counter examples to prove this notion wrong I would appreciate them.
I take you example of the broken computation:
v1 = v0 * (t1 / t0) - a
A smart lint system with a vocabulary for physics programs could know by convention that a name t means time and 0 and 1 means index and that in context of time the greater index means a step ahead in time. (At least this is what 90% of humans would assume). So it could infer t1 > t0 and check that at runtime in some debug mode.
Maybe there are valid cases where t1 < t0 but then this naming introduces under guarantee false human interpretations of the source.
The lint system should model and check against the typical human interpretation of names.
This does not detect the above wrong computation but it could help find errors without writing a test for every function.
Hmm. Isn't a lint system as you describe just an informal static typing system in this case? And anyway, someone still needs to write the lint system. Adding layers of abstraction does not make the problem go away...
Sure, when we have well defined domain logic rules those can be enforced through typing. But I would claim it is really unusual to do greenfield development and start from a really well defined set of domain logic rules formalized as a type system. Usually one discovers those rules as one develops the system, and then encodes those rules in types.
Yeah, physical dimensions are one of the few concrete static types one can beneficially leverage at the start of a project. They describe an uncommonly well defined domain logic polished over centuries. What I tried to demonstrate that algebraically correct expression does not necessarily imply correct domain logic and a physics calc was the most simple example I could come up wit.
Too bad only a few languages like F# come with dimensions attached to numbers out of the box :)
