Re: Of Legal Language and CS Notation

[Geoffrey Knauth <address@hidden>]

Shriram asked Peter Wasilko:
> do you eschew legal language when speaking about
> legal matters to a fellow member of the bar?

Peter answered:
> lawyers don't really talk that way other than to key in on issues.

This made me think about how, at a high level of sport (world class 
rowing), coaches talk to athletes.  They share a common technical 
language, but what drives performance is expressiveness.  A successful 
coach expresses what he wants in different ways until suddenly an idea 
forms in the athlete's mind and a concept sticks.  Athletes tire of 
coaches who just repeat the same formulae.  Dullard coaches think of 
athletes as replaceable cogs.  Athletes are unique persons and 
legendary coaches have limitless imagination with which to reach those 
athletes' minds.

How does this relate to the previous discussions about type theory?  
Programmers are athletes, experts are coaches.

People say programming is an Art.  It is also Sport.  Sport is fun.  
Great programmers arise because they want to have fun, they want to 
scale the next Everest, they want to explore new territory.  Type 
theory is a lifeboat and a survival kit, not the anchor it is perceived 
to be ("By the time I read all those papers, I'll be dead!").  We need 
to recast type theory as an enabler for safe long-range exploration.

Geoffrey
--
Geoffrey S. Knauth | http://knauth.org/gsk