Bitc: a safe systems programming language

Modern programming languages support the development of correct, high-performance application software by providing features such as static type safety, sound and complete type inference, higher-order functions, polymorphism, and mathematically well-founded semantics. Systems software, such as device drivers and operating system kernels, imposes the unique requirements of prescriptive data structure representation and generic mutability support on languages used for its development. Modern programming languages—particularly those that support type inference—do not support complete mutability and prescriptive data structure representation. In consequence, systems codes continue to be built in languages such as C and C++ without the benefits of modern programming language principles and tools. This dissertation presents BitC, the first language to support principal polymorphic type inference in the presence of C-style representation control and mutability. BitC's type system features a new mutability model that combines unboxed types with a consistent typing of mutability. The type system is provably sound, supports polymorphism, and eliminates the need for alias analysis to determine the immutability of a location. A sound and complete inference algorithm for this type system, which automatically infers both mutability and polymorphism, is presented. The dissertation presents an evaluation of BitC's effectiveness as a systems programming language with respect to expressiveness as well as performance. It demonstrates that key data-structures, algorithms and programming idioms used in systems programming can be safely written in BitC. Early measurements on performance critical programs (ex: SHA1 hash computation) suggest that the performance of these routines written BitC is comparable to their native C implementations.