Coq has an interesting compromise, where the actual code passed to the compiler is in ASCII, but one can define sequences which have alternative renderings (usu

Coq has an interesting compromise, where the actual code passed to the compiler is in ASCII, but one can define sequences which have alternative renderings (usually to attempt to visually match existing math notation). For example, one could write Theorem demo: forall (x: nat), (exists y, x = S y) -> x <> 0. In many editors, this will get rendered as Theorem demo: ∀ (x: ℕ), (∃ y, x = S y) → x ≠ 0. This looks a lot nicer for mathematicians. (S here is Peano successor.) One minor nuisance is that, without an additional plugin, you can't actually write source code literally using the Unicode symbols (they're normally display-only, not part of a source file). The plugin to allow one to type them explicitly (with a Unicode-aware input method) does exist, but would make one's source code not portable for other users. Also, this is really specifically for math, not internationalization, and doesn't provide a helpful model for people wanting to type identifiers in non-ASCII-supported scripts.