Abstract Pluggable Type Systems

Traditionally, statically typed programming languages incorporate a built-in static type system. This system is typically mandatory: every legal program must successfully typecheck according to the rules of the type system. In contrast, optional type systems are neither syntactically nor semantically required, and have no effect on the dynamic semantics of the language. This in turn enables pluggable type systems [Bra03, Bra04], allowing multiple type systems to be used simultaneously and/or sequentially for various semantic analyses. We argue that pluggable types can provide most of the advantages of mandatory type systems without most of the drawbacks. 1 Mandatory Typing Considered Harmful Mainstream programming languages incorporate mandatory type systems. These type systems are widely perceived to enhance software reliability and security, by mechanically proving program properties. Paradoxically, such mandatory type systems inhibit software reliability and security, because they contribute to system complexity and brittleness