I really dislike unicode slop in code. I was contributing proofs about insertion sort to the lean cslib project. The project has a mechanism to count operations to prove things about complexity. To say an operation takes one "tick" of time you have to surround that operation with a tick function(Its some Monad shit I don't get it). The "tick" function has a unicode ✓ as notation. Why? What purpose does this serve? Allowing programmers to make up operators was a mistake.