It was Reynolds who observed that types are useful for syntactically enforcing levels of abstraction, and what that really meant to Reynolds is that one can locally establish invariants for -- and change private representation of -- abstract data types (ADTs), without affecting the observable behavior of code that relies on those types. From my perspective, the crucial point here is that types *enable* programmers to write more reliable code because the burden of establishing invariants on an ADT is kept *local* to the module that defines it. The restrictions of the type system then guarantee that the rest of the program, by virtue of being forced to respect the abstraction of the ADT, is also forced to respect the ADT's locally-established invariants. Thus, the very restrictiveness of types is what enables program *correctness* to scale.