RE: Help with type advocacy

To: "'Ken Shan'" <ken@digitas.harvard.edu>, types@cis.upenn.edu
Subject: RE: Help with type advocacy
From: Robert Harper <Robert.Harper@cs.cmu.edu>
Date: Thu, 4 Oct 2001 18:11:59 -0400
Hi Ken:

In this sort of situation I often spin my yarn around Reynolds's beautiful
one-liner:

	A type system is a syntactic discipline for enforcing levels of
abstraction.

It's all there: part of the syntax (not a "comment"), its enforced, and what
it enforces are levels of abstraction.

I often augment the discussion with the remark that types impose invariants,
and that therefore stricter type systems give you stronger properties.

Good luck!
Bob Harper

-----Original Message-----
From: Ken Shan [mailto:ken@digitas.harvard.edu]
Sent: Thursday, October 04, 2001 4:25 PM
To: types@cis.upenn.edu
Subject: Help with type advocacy


[----- The Types Forum, http://www.cis.upenn.edu/~bcpierce/types -----]

Hello all,

I am preparing a three-minute talk to tell incoming graduate students
at my school about types.  People come here to do all sorts of
research -- network protocols, natural language processing,
cryptography, etc.  This is not a joke, and "three" was not a typo.

My goal is not to get people to become type system researchers or
switch to a new programming language overnight.  My goal is to
introduce them to tools and ways of thinking they may not be
previously aware of that may help them understand problems better and
produce better code -- some of which may even be applicable to C.

The following is my current outline/slide-draft.  I am seeking advice
on all aspects of this presentation; I may even be convinced that it
is impossible to achieve my goal in three minutes.

    Before implementing a solution, first understand what the problem
    is and what constitutes a solution.

    If your program crashes, it is not a solution.
    If your program hangs, it is not a solution.
    If your program produces the number "foo", it is not a solution.
    ==> These fundamental necessities are called _safety properties_.

    Types are proofs of safety that machines can manipulate.
    - Machines can easily check and infer types.
    - Humans can easily read and write types.
    - Types help both humans and machines understand code.

    Types help eliminate memory leaks and segmentation faults.
    Types help preserve the integrity of data representations.
    Types help document and verify program invariants.
    ==> Mistakes that can be automatically located, should be.

I want to add a final section of "pointers" -- things that the
intrigued should look into: programming languages, techniques, even
papers.  What pointers should I give?

  - Programming languages:
        Cyclone
        ML
        Haskell
        Clean
  - Programming techniques:
        _Effective C++_
        _Writing Solid Code_
  - Papers:
        Luca Cardelli, _Type Systems_
        Daniel Wang, _Why I Like Types_

Thanks in advance.

-- 
Edit this signature at http://www.digitas.harvard.edu/cgi-bin/ken/sig
For this reason a man will leave his father and mother and be united to
his wife, and they will become one flesh.