Going through a single line of text to understand a concept is much better than having to go through two or more. I believe you should understand that, if your definition of conciseness matches mine.

As a programmer, you know first hand that repeating oneself is bad practice: it's better to define a function which will encapsulate this computation you need to repeat rather than using copy and paste. The same goes for any language: having vocabulary to embody reccuring ideas helps us discuss complex ideas more easily.

> Do you really need to express concepts with a single strange character?

It is only strange to you because you don't speak greek. Of course many don't: my pedantic point is that Greeks might disagree with you about these characters being strange, and less pedantically, the scientific community will argue that it's not that strange when you belong to their group. There are only a handful of them to remember in the context of type theory.

I guess you would want these characters, like Gamma (Γ), Delta (Δ), tau (τ) or sigma (σ) to be replaced by their ascii equivalent (eg. G, D, t, s), or perhaps even more evocative names? But even if this would be done, you'd still have to understand the underlying concepts they represent, such as the typechecking context which is usually represented by Gamma.

These concepts are indeed not easy to understand: you would have to learn to become a Gorilla in order to be able to hold that banana you languish for, or survive in the Jungle that surrounds it.

One good thing about using a different character set is that they stand out. There's little chance to confuse them with words of vernacular English. Greek mathematicians actually might have a harder time with these notations than you do :)