Re: if vs. when vs. and: style question

[Rusi]

On Monday, March 30, 2015 at 7:25:42 AM UTC+5:30, Óscar Fuentes wrote:
> Another issue is related to what Pascal Bourguignon mentions, and my
> reply to Stefan: the abundance of symbols adds mental strain.
> Furthermore, using shorter textual representations for objects makes the
> code almost cryptic, moreso when such representations uses symbols taken
> from a large pool. That's my experience and, IIRC, there are studies
> that back that impression.

One of the most fundamental DNAs of a programmer is what we may call
'batch-moding'  Examples from more specialized to more universal:

- preprocessing string search to get fancy algorithms like KMP
- Use a compiler rather than an interpreter
- Write a program (to do a computation) rather than do the computation
 (on pen-paper)

The same principle applies to the wetware in the box atop our shoulders.
So if you take Stefan's



has_type env exp type

vs
   
Γ ⊢ e : τ 

The first is ok and preferable to the second if its to be written once 
(or a few times).  As it becomes increasingly frequent the demand for
(something like) the second will correspondingly increase.

"Something like" because

Stefan: 
> Some of those letters/signs have meaning shared within a fairly large 
> mathematical
> community while others are much more specific to a specialized subfield.

Here are TWO points that are separate and deserve orthogonalization
1. Mathematicians do good compression of their subject
2. Mathematics is a cottage industry – one uses gzip, one LZ, one good-old 
huffman

Many arguments seemingly against the first, are under the hood, arguments 
against the second.

> The usual advice about descriptive names and
> self-documenting code applies.

Yes... Between


has_type env exp type

vs
   
Γ ⊢ e : τ 

Some will find the second frightening; the first ok
Some will find it exactly the opposite -- "prose" and "prolix" are quite close

How much are these judgments objective? Genetic-structural? Just plain
illiteracy/bad-habits??  Open questions...
[And questions unrelated IMHO to the systems used by a certain Mr. Noah to 
design a large boat on which our ancestors were collected]
-------------------
tl;dr Unicode is an ISO standard – something mathematicians have never heard of.
Seems like a good idea to take their knowledge and discard their ignorance