The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Makarius,

> I fully agree that high-end proof assistants should support proper
> mathematical symbols without the user having to think about it. I disagree
> that such a blissful situation can be equated with "Unicode". Unicode is a
> rather big standard with many sub-standards, and it requires years and
> decades to make it really work for a particular task.

I see that I was a bit simple minded here. I have quite some experience with 
supporting languages like Japanese or Russian in my SW, but I see that 
supporting math is a completely different story. I guess it boils down to the 
fact that OSes don't have a language package for "math" as they have for e.g. 
Japanese. Maybe this is what we should try to achieve long term. E.g. not 
only math fonts but a SW independent math IME (the thing in an OS which 
converts what you type to Unicode characters). Coming back to the subject of 
this thread: there is some hope.

Best regards,

Michael
Intel Deutschland GmbH
Registered Address: Am Campeon 10-12, 85579 Neubiberg, Germany
Tel: +49 89 99 8853-0, www.intel.de
Managing Directors: Christin Eisenschmid, Christian Lamprechter
Chairperson of the Supervisory Board: Nicole Lau
Registered Office: Munich
Commercial Register: Amtsgericht Muenchen HRB 186928