I'm surprised nobody so far has mentioned Agda (http://wiki.portal.chalmers.se/agda http://wiki.portal.chalmers.se/agda). Not only does it allow the use of unic

I'm surprised nobody so far has mentioned Agda (http://wiki.portal.chalmers.se/agda http://wiki.portal.chalmers.se/agda). Not only does it allow the use of unicode in identifiers, but it uses them extensively throughout its standard library. After using Agda for a while, one quickly realises that most of the issues raised in this thread are rather unimportant. Having extra brackets, more equality symbols and greek letters available really does make code nicer to read when used judiciously.