‹Programming› 2024
Mon 11 - Fri 15 March 2024 Lund, Sweden
Wed 13 Mar 2024 16:15 - 16:45 at M:Teknodromen - Research Papers 3 Chair(s): Tijs van der Storm

Context: Roblox Studio lets millions of creators build interactive experiences by programming in a variant of Lua called Luau. The creators form a broad group, ranging from novices writing their first script to professional developers; thus, Luau must support a wide audience. As part of its efforts to support all kinds programmers, Luau includes an optional, gradual type system and goes to great lengths to minimize false positive errors.

Inquiry: Since Luau is currently being used by many creators, we want to collect data to improve the language and, in particular, the type system. The standard way to collect data is to deploy client-side telemetry; however, we cannot scrape personal data or proprietary information, which means we cannot collect source code fragments, error messages, or even filepaths. The research questions are thus about how to conduct telemetry that is not invasive and obtain insights from it about type errors.

Approach: We designed and implemented a pseudonymized, randomly-sampling telemetry system for Luau. Telemetry records include a timestamp, a session id, a reason for sending, and a numeric summary of the most recent type analyses. This information lets us study type errors over time without revealing private data. We deployed the system in Roblox Studio during Spring 2023 and collected over 1.5 million telemetry records from over 340,000 sessions.

Knowledge: We present several findings about Luau, all of which suggest that telemetry is an effective way to study type error pragmatics. One of the less-surprising findings is that opt-in gradual types are unpopular: there is an 100x gap between the number of untyped Luau sessions and the number of typed ones. One surprise is that the strict mode for type analysis is overly conservative about interactions with data assets. A reassuring finding is that type analysis rarely hits its internal limits on problem size.

Grounding: Our findings are supported by a dataset of over 1.5 million telemetry records. The data and scripts for analyzing it will be available in an artifact.

Importance: Beyond the immediate benefits to Luau, our findings about types and type errors have implications for adoption and ergonomics in other gradual languages such as TypeScript, Elixir, and Typed Racket. Our telemetry design is of broad interest, as it reports on type errors without revealing sensitive information.

Wed 13 Mar

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

15:15 - 16:45
Research Papers 3Research Papers at M:Teknodromen
Chair(s): Tijs van der Storm CWI & University of Groningen
15:15
30m
Talk
Coqlex: Generating Formally Verified LexersVol. 8
Research Papers
Wendlasida Ouedraogo INRIA Saclay, Gabriel Scherer INRIA Saclay, Lutz Strassburger INRIA Saclay
Link to publication DOI
15:45
30m
Talk
McMini: A Programmable DPOR-based Model Checker for Multithreaded ProgramsVol. 8
Research Papers
Maxwell Pirtle Northeastern University, Luka Jovanovic Northeastern University, Gene Cooperman Northeastern University
Link to publication DOI
16:15
30m
Talk
Privacy-Respecting Type Error Telemetry at ScaleVol. 8
Research Papers
Ben Greenman University of Utah, Alan Jeffrey Roblox, Shriram Krishnamurthi Brown University, Mitesh Shah Roblox
Link to publication DOI