Subject: [Fwd: Help with type advocacy]
From: Craig Chambers (chambers@cs.washington.edu)
Date: Thu Oct 04 2001 - 18:18:11 PDT
FYI.
Robert Harper wrote:
>
> [----- The Types Forum, http://www.cis.upenn.edu/~bcpierce/types -----]
>
> 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.
_______________________________________________
Cecil mailing list
Cecil@cs.washington.edu
http://majordomo.cs.washington.edu/mailman/listinfo/cecil
This archive was generated by hypermail 2b25 : Thu Oct 04 2001 - 18:19:03 PDT