Soundness challenges in typed racket fixed with semantic proof
Revisiting Soundness for Occurrence Typing, Semantically
Programming Languages
Summary
Programming languages sometimes use clever ways to check if programs are correct, but these methods can have tricky gaps that make them unreliable. The authors studied one popular system called Typed Racket and found errors in its formal foundation that also affected some other systems and even the actual Typed Racket language. They fixed these errors by redesigning the core system and proving correctness using a more reliable mathematical method, making the system simpler and more trustworthy.
What this means in practice
- •For programming language designers: Improve type systems by applying a semantic proof approach to avoid foundational soundness bugs seen in occurrence typing systems like Typed Racket.
- •For static analysis tool developers: Build more reliable static analyzers for dynamically typed languages using soundness guarantees from the revised Typed Racket calculus and semantic proofs.
A theory result. No direct application yet.
Authors
Yuquan Fu, Carlo Angiuli, Sam Tobin-Hochstadt
Abstract
Over the past two decades, numerous systems have brought some of the benefits of dependent typing to a wide variety of new programming languages, often by restricting which terms can appear inside types. Such techniques are known as refinement types, occurrence typing, liquid types, and path dependent types, among others. However, the restrictions adopted by these systems often break the substitution property, because they explicitly disallow the ability to substitute arbitrary terms for variables inside types. This leads to significant complexity in the design and metatheory of these systems, increasing the possibility of significant errors. We consider a specific line of work on occurrence typing, namely, the calculus underlying Typed Racket due to Tobin-Hochstadt and Felleisen 2010. We show that the fundamental challenge of substitution into types resulted in multiple flaws in the formalism and the syntactic type soundness theorem of this work. These flaws are replicated in several other papers building on this work, and also surface as a soundness bug in Typed Racket itself. We identify and repair these problems, revising the core calculus of Typed Racket and giving a \emph{semantic type soundness} proof using step-indexed logical relations, formalized in Lean. We argue that this approach is simpler than it may seem, and easily scales to handle the complexity of the occurrence typing in Typed Racket.