[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

The Accessibility of Type Theory Research

> > On 2003-11-19T14:28:15-0800, James McCartney wrote:
> > Well a summary might be useful for people who cant' read this stuff:
> > [gibberish afaict]
> Given that I don't think anyone can read what you put down, I would
> completely agree that a summary might be useful for people who can't
> read it, in other words people in geeral.  But I'm not clear what your
> point is...?

I think this was intended as a critique of the accessibility of the
notation used to express the Operational Semantics of modern type
theory, which seems to demand a somewhat greater level of mathematical
sophistication than most average language aficionados bring to the

Thus to say that it takes more than one pass for most people to fully
grok the chapters of Pierce would be putting it mildly.

Now if anyone could point to a good paper on how to read type theory
papers and mentally parse their notation into something closer to
English, perhaps it would be easier to access the research in this area.

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?

I think I'm feel myself being drawn into Shriram's fourth category.

--- Peter


Peter J. Wasilko, Esq.
     J.D., LL.M.               

Executive Director, The Institute for End User Computing, Inc.

Visit us on the web at: http://www.ieuc.org


It's time to abandon brittle architectures with poorly factored
interfaces, gratuitous complexity, and kludged designs dominated
by sacrifices on the altar of backwards compatibility.

Such artifacts are vulnerable to cyber-attack, weigh down the
economy costing trillions of dollars in lost productivity, and
suffer from an impoverished conceptual model that lacks the
integration and elegance needed to empower end users to
get the most from advanced applications in the future.

The Institute for End User Computing --- Pursuing Secure, Simple, 
   Supple, & Sophisticated Systems to Unlock Our Human Potential

* The Institute is incorporated under New York State's
   Not-For-Profit Corporation Law