Programmers as Athletes

Geoffrey Knauth made an interesting post on the ll1 mailing list. The topic was whether programmers (and programming language designers) should try to learn about advanced type theory, or whether type theorists should try to make their work more accessible to programmers.

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.

I think he makes two good points, even though he implies that they're actually the same. The first point is that different people have different ways of working and of conceptualizing problems. The second point is that if you want to do technically difficult work, you would do well to take advantage of tools that make the task easier or more reliable (e.g. type theory), even if using those tools is challenging in its own right.

Interestingly, this is the same mailing list thread that triggered my post about Shriram's textbook.