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.
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.
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.
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.
The space of physically meaningful equations is vastly smaller than the space of all possible permutations of variables and operators.
Too bad only a few languages like F# come with dimensions attached to numbers out of the box :)