[mullr]

you mean like 'u' for micro, and 'lambda'? I think this is pretty common.

Regardless, you're probably doing yourself a disservice if you're allowing things like that to take choices out of your toolbelt. Perhaps the worst offender is TLA+, where you have to write actual ascii art and latex inside your code (yes, I know model/spec). I despise it, to be clear, but it's still a pretty good tool and often the right thing to reach for

[exdsq]

Or Agda where you basically have to use emacs with the agda extension to get all the characters.

Less than or equal ends up looking like:

data _≤_ : ℕ → ℕ → Set where

   z≤n : {n : ℕ} → zero ≤ n

   s≤s : {n m : ℕ} → n ≤ m → suc n ≤ suc m

[mullr]

And to really rub salt on it, they have a syntax that looks very much like stock latex for math symbols, and SOME of them are the same, but not all of them! (all / forall is the one that comes to mind, it's been a little while)

[hwayne]

It always ALWAYS trips me up that TLA+ uses \A and \E while LaTeX uses \forall and \exists