This paper presents recent work on the Luau programming language which is used for, amongst other reasons, scripting games. We talk about the human aspects of the Luau type system, and in particular, how large the heterogeneous developer community is for Luau. We then talk about two recent developments in Luau, in particular gradual type and semantic subtyping.
Our presentation of gradual typing is different from others and uses type error suppression.
Our definition of "pragmatic semantic subtyping" drops the set theoretic requirement from the original development of semantic subtyping, resulting in a simpler presentation of an algorithm for subtyping.
These recent developments have been implemented in production Luau, and mechanically verified in Agda for a core Luau.
Anyone who wants to ask about recent work, or the last 30 years of a varied CS career, should feel free.
