I really want to agree with you about the extended character set. Much of it is totally cosmetic even. But when you get to reading more advanced things the ASCII overload begins and nice notation becomes key. Coq/Agda/Idris all embrace this out of necessity essentially.