Most dependently-typed languages support unicode. Both adga and lean support unicode (in functions) and designing your custom operators. It's very useful to write proofs about math: Here's a simple example from Lean: lemma le_lim {x y : ℝ} {u : ℕ → ℝ} (hu : seq_limit u x) (ineg : ∃ N, ∀ n ≥ N, y ≤ u n) : y ≤ x := begin -- sorry apply le_of_le_add_all, intros ε ε_pos, cases hu ε ε_pos with N hN, cases ineg with N' hN', let N₀ := max N N', specialize hN N₀ (le_max_left N N'), specialize hN' N₀ (le_max_right N N'), rw abs_le at hN, linarith, -- sorry end