The Coq mailing list

[Jonathan Leivent <jonikelee AT gmail.com>]

On 03/03/2016 11:42 AM, Clément Pit--Claudel wrote:
> 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.

I'll put in a plug for Clémen's work, as well.  I am a SW engineer 
trying to come to terms with this issue, and the prettification 
mechanism offered by Company Coq is a very good compromise. However, it 
ties those who want the prettification to the Emacs/PG/Company-Coq 
toolset.  Not that there's anything wrong with that.

As to Michael's comment: I'm not sure it is audio/language centric vs. 
visual centric, but perhaps an explanation doesn't really matter.  What 
matters is that many SW engineers will see such symbol usage as an 
impediment.

-- Jonathan