Well-typed Programs Can Go Wrong: Enhancing the Reliability of Type Checkers in Compilers-Thodoris Sotiropoulos |LambdaDays24

[CodeSync]

Well-typed Programs Can Go Wrong:(…)Type Checkers in Compilers-Thodoris Sotiropoulos |LambdaDays24

Well-typed Programs Can Go Wrong:(...)Type Checkers in Compilers-Thodoris Sotiropoulos |LambdaDays24

This talk was recorded at Lambda Days in June 2024. If you’re curious about our upcoming event, check https://lambdadays.org

Abstract
Static typing in programming languages is crucial for robust software development. Flaws in type checkers lead to (1) reliability and security ramifications on the programs compiled with the faulty compilers, and (2) degradation of the programmers’ experience and productivity. In particular, compiler typing bugs typically cause frustrating rejections of well-typed programs, dangerous acceptances of erroneous, type-unsafe programs, or annoying crashes and compilation performance issues.

In this session, I will present our ongoing efforts on enhancing the reliability of compilers’ type checkers using randomized software testing. Within three years, we have found more than 250 bugs (of which 140 bugs have been fixed) in industrial-strength compilers, such as Java, Kotlin, Scala, and Groovy. Most of the discovered bugs lie in critical components of type checkers, including type inference, parametric polymorphism, overloading, or higher-order functions.

Comments welcome! View the code-sync tag for more Code Sync talks!