> As long as any char doesn't have a special meaning (e.g. in Agda "(", ";", "," etc have special meanings) you can use it in an identifier. The trade-off is that
I would say the trade off is variable names like “a+b” themselves. I fail to see any reason why would I want something like that, like even in Math where the grammar is very hand-wavy to accommodate human parsing you would be insane to write that (though to be fair, math does have their own share of problem with identifiers, enumerating all the letters in different alphabets is not a sustainable solution)
Why not just give it some temporary name, like ‘t’, supposedly it is only used in a very tight scope. Haskell and similar languages often do these things with `let in ..` or `.. with t=a+b`.
Not really better at all, but I feel this is a bit contrived example. If it really is just numeric addition that just let the compiler do its job, otherwise I’m sure there are better names for whatever you actually try to do. And, random helper variables are a thing even in math, you don’t name the thing the way you calculate that thing because then you don’t spare any character.
I would say the trade off is variable names like “a+b” themselves. I fail to see any reason why would I want something like that, like even in Math where the grammar is very hand-wavy to accommodate human parsing you would be insane to write that (though to be fair, math does have their own share of problem with identifiers, enumerating all the letters in different alphabets is not a sustainable solution)