Casanova: a declarative language for safe games

Games are extremely complex pieces of software which give life to animated virtual worlds. Games require complex algorithms, large worlds filled with many intelligent entities and high-quality graphics, and it all must run in real time. Building general, high-performance frameworks capable of represent- ing any virtual world has, until now, proven to be an elusive task; existing solutions either sacrifice performance (X3D browsers) or generality (game engines). In this paper we present a model that formalizes our notion of a correct game. This model gives all the important properties that game developers struggle to maintain by hand, that is the strong normalization of the tick function, the independence from the order of the ticks of each entity, and the fact that all active entities of the game state must be ticked exactly once. We define the Casanova language around this model, with the aim of achieving the threefold objective of creating games that are correct, declarative (and thus simpler to write) and fast to run. We will use a linear type system to enforce the uniqueness of our entities (to ensure exactly one tick for each) and to ensure that ticks do not have overlapping effects. We will impose certain restrictions on the state to avoid infinite loops in the update function (in the shape of cyclic references) and we will use a specialized type system to make sure that all the active coroutines of the game will always yield.