Check out Lean Prover's online editor:
https://leanprover.github.io/live/latest/They borrow syntax from LaTeX math-mode to allow symbol entry, such that you can type "\ne" and as soon as you hit the space after the "e", you get ≠ instead.
The language plugin for Visual Studio Code does the same thing.
Lean Prover's not exactly a programming language, but :
def foo (a b : ℕ) : ℕ → ℕ → ℕ :=
λ a b, a + b
Still looks decent.
I think it has to be all or nothing though, since if it's optional the odds of getting decent editor support for it is low.
