We are tending towards assign-once variables.
Why do we need variable names, if the variables are not variables?
Example:
plus( b : integer, c : integer) : integer
becomes
plus (integer, integer) : integer
and, in the presence of type synonyms, becomes
plus (b, c) : a
a = integer
b = integer
c = integer
[N.B. in the last case, the checker can insist on unique names for all parameters and return types. This, IMO, is makes the checker simpler, while preserving DI.][1]
[1] Design Intent