Using math symbols for operators

I will briefly mention Adga, a dependently typed language used for theorem proving. It goes all-in on Unicode, using it everywhere for operators.

Years ago, I had a lot of trouble as a new user of Agda because it wasn’t clear how to type the operators I needed to do basic things, and if I remember correctly the official docs only had editor integration for Emacs. And I was not interested in learning a new (complex) text editor on top of a new language at the same time.

These days I personally have system-wide text replacement for very many emoji & Unicode symbols, so I can type :+1<space> and get :+1: for example. But I don’t expect those I work with to have similar systems already set up.

1 Like