Date Added: Jan 2012
Static type systems are the world's most successful application of formal methods. Types are simple enough to make sense to programmers; they are tractable enough to be machine-checked on every compilation; they carry no run-time overhead; and they pluck a harvest of low-hanging fruit. It makes sense, therefore, to seek to build on this success by making the type system more expressive without giving up the good properties the authors have mentioned. Every static type system embodies a compromise: it rejects some "Good" programs and accepts some "Bad" ones. As the dependently-typed programming community knows well, the ability to express computation at the type level can improve the "Fit"; for example, they might be able to ensure that an alleged red-black tree really has the red-black property.