The Coq mailing list

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

Dear Enrico,

> This is why I asked if a relicensing coming from him would help.
> I think I could have some grip on this topic, given we share a common
> background on free software.  Also, his (to my taste) hilarious license was
> designed as a pun to GPL-vs-BSD zealots, not to annoy companies.

If I would know Sam personally, I would definitely try to make him aware of 
the issues.

Btw.: do you think that keeping Unicode input outside of CoqIDE is the right 
way to go?

One interesting point is that I had a discussions with a SW engineer on this 
topic today and he really doesn't like special notations for things like 
forall or exists. He believes that many SW engineers might be repelled by 
such notations, because they are not used to it. I argued that doing math to 
a certain extent uses the visual capabilities of the brain and that this 
requires a notation which can be visually processed, but I don't think I 
could convince him. Maybe there are people who a more audio/language centric 
and others who are more visual centric and that this influences which 
notations you prefer.

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