Oh god, this. I want a language that as I type, != Gets replaced with a proper ≠ not equals sign and proper symbols for AND, OR, and NOT.
https://www.hanselman.com/blog/MonospacedProgrammingFontsWit...
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
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.