Devoxx Greece 2024 - Well-typed Programs Can Go Wrong: Enhancing the Reliability of Type Checkers...

Full Title : Well-typed Programs Can Go Wrong: Enhancing the Reliability of Type Checkers in Compilers Speaker : Thodoris Sotiropoulos Static typing in programming languages is crucial for robust software development. Recently, it has been shown that the static typing implementations of well-established compilers suffer from a substantial number of bugs. These implementation flaws 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 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, including critical soundness compiler bugs. This talk will inform developers about the pitfalls in software development process introduced by faulty compilers, along with the associated impact. At the same time, I will provide highlights for language designers and compiler engineers about which language features are the hardest to get right and implement. Finally, this talk will present one of the most recent advancements in compiler and programming language testing, which also involves applications in other domains, such as library and API testing.