I’m not defending either standard Unicode identifiers or C Unicode identifiers (which are, incidentally, very different things, see WG14/N1518), no :) The Agda people make good use of various mathematical operators, including ones that are very close to the language syntax (e.g. colon as built-in type ascription and equals as built-in definition, but Unicode colon-equals as a substitution operator for a user-defined type of terms in a library for processing syntax), but overall I’m not convinced it’s worth it at all.
As a way to avoid going ASCII-only, though, excluding only things that look like syntax might be simultaneously not going far enough (how are homograph collisions between user-defined identifiers any better?) and too far (reliably transplating identifiers between languages that use different sets of punctuation seems like it’d be torturously difficult).
As a way to avoid going ASCII-only, though, excluding only things that look like syntax might be simultaneously not going far enough (how are homograph collisions between user-defined identifiers any better?) and too far (reliably transplating identifiers between languages that use different sets of punctuation seems like it’d be torturously difficult).