The Coq mailing list

[Clément Pit--Claudel <clement.pit AT gmail.com>]

On 03/03/2016 08:59 AM, Soegtrop, Michael wrote:
> 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.

I think prettification offers an interesting middle ground (see an example at 
https://github.com/cpitclaudel/company-coq/#prettification-of-operators-types-and-subscripts;
 these two screenshots show the same Emacs buffer, with and without the 
prettification layer). This should allow both kinds of SW engineers to work 
on the same files. 

Clément.

Attachment: signature.asc
Description: OpenPGP digital signature