Agda embraces Unicode. PureScript & Haskell (with the UnicodeSyntax extension) both behave pretty well with a lot of Unicode operators (but rely on bicameral scripts as the leading character for deciding if something like a value or a Constructor/Type). Not sure of its status, but ocaml-m17n is a way to get some Unicode support in OCaml which otherwise can’t deal with any of it.
Agda goes above and beyond that when you consider their mix-fix syntax…
While it might not be perfect, it’s a hella lot closer to mathematical proving/programming with normal functional programming “constructs” (for lack of a better word… idris etc, also the struggle with sized types)
