[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: Of Legal Language and CS Notation
Shriram asked Peter Wasilko:
> do you eschew legal language when speaking about
> legal matters to a fellow member of the bar?
> 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
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 S. Knauth | http://knauth.org/gsk