An Argument against Gradual Type Systems in Programming Language Semantics

In 2006, Jeremy Siek and Walid Taha formalized the concept of gradual type systems, which integrates static and dynamic typing in a single programming language. This allows the programmer to statically or dynamically type portions of their code at will, which offers more flexibility than languages that require all code to be statically typed. Despite the added convenience, gradual typing comes with its own set of tradeoffs, and researchers have been debating whether the drawbacks of integrating static and dynamic types outweigh its benefits. This thesis builds off of previous research to investigate the advantages and disadvantages of using a gradual type system, specifically in the context of formal programming language theory, through the usage of structural operational semantics and Harper's progress and preservation approach of proving type safety.