RE: Help with type advocacy
In this sort of situation I often spin my yarn around Reynolds's beautiful
A type system is a syntactic discipline for enforcing levels of
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.
From: Ken Shan [mailto:email@example.com]
Sent: Thursday, October 04, 2001 4:25 PM
Subject: Help with type advocacy
[----- The Types Forum, http://www.cis.upenn.edu/~bcpierce/types -----]
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:
- Programming techniques:
_Writing Solid Code_
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.