Re: The Accessibility of Type Theory Research

[Russ Ross <address@hidden>]

On Wed, Nov 19, 2003 at 10:49:03PM -0500, Peter J. Wasilko wrote:
> But more to the point, if a significant fraction of the language
> designers on this list have a hard time penetrating the language of
> papers that deal with the tradeoffs among alternate typing schemes and
> annotation styles, how can we expect language implementors to make
> effective use of this research or for average programmers to make
> effective use of tools that embody it?

It's true that specialized languages can be difficult to penetrate,
but they usually exist because other languages weren't up to the job
of expressing the intended ideas.  You can probably get there in the
end, but the translation will be longer, more error-prone, and
probably more complicated as a result.

The first time I came across the halting problem was in my early
teens, and it was in some awful book intended for hobbyists.  The
author didn't want to confuse people with Turing machines, so he
discussed it all in terms of C programs and in the end he really
ruined it.  I found flaws in his reasoning and came away believing
that the halting problem was probably insignificant if it was even
correct in the first place.  It wasn't until years later in college
that I learned the notation and theory behind it and came to
actually understand as well as appreciate it.

Hopefully, someone translating semantics papers into less technical
language would do a better job, but I fear he would expose himself
to the same risks.  In the end, it will be watered down, ambiguous,
and probably wrong.  It might be good for people surveying the ideas
for personal interest, but anyone intending to extend the work or
implement the ideas (or hold a meaningful debate about them) will
just have to learn the notation and go to the sources anyway.
That's why the notation is there: it's concise, well defined, and
appropriate to the problems at hand.

If you want to be someone's student, ask him/her to bring the
discourse down to your simplified level.  If you want to challenge
his/her ideas, you'd be better off fully understanding them first.

- Russ