luau-lang/luau
1
0
Fork 0
mirror of https://github.com/luau-lang/luau.git synced 2025-04-08 04:40:54 +01:00
Code Issues Projects Releases Packages Wiki Activity

Got the HATRA paper back down to 4pp+bib

Browse source
This commit is contained in:
ajeffrey@roblox.com 2021-07-19 16:14:25 -05:00
parent 38b52ff21b
commit 81599cc78d
2 changed files with 2 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

BIN
papers/hatra21/hatra21.pdf
View file

Binary file not shown.

7
papers/hatra21/hatra21.tex
View file

@ -56,7 +56,6 @@ approximately 20~million experiences available on Roblox, created
by 8~million developers. Roblox creators are often young, for by 8~million developers. Roblox creators are often young, for
example there are over 200~Roblox kids' coding camps in 65~countries example there are over 200~Roblox kids' coding camps in 65~countries
listed at~\cite{AllEducators}. listed at~\cite{AllEducators}.
The Luau programming language~\cite{Luau} is the scripting language The Luau programming language~\cite{Luau} is the scripting language
used by developers of Roblox experiences. Luau is derived from the Lua used by developers of Roblox experiences. Luau is derived from the Lua
programming language~\cite{Lua}, with additional capabilities, programming language~\cite{Lua}, with additional capabilities,
@ -266,8 +265,7 @@ $(\IF f() \THEN \ERROR \END)$ will produce a runtime error when $f()$ is
$\TRUE$, but we can aim for a weaker property, that all flagged code $\TRUE$, but we can aim for a weaker property, that all flagged code
is either dead code or will produce an error. Either of these is a is either dead code or will produce an error. Either of these is a
defect, so deserves flagging, even if the tool does not know defect, so deserves flagging, even if the tool does not know
which reason applies. For example, using this definition which reason applies.
$(\IF f() \THEN \squnder{\ERROR} \END)$ is not a false positive.
We can formalize this by defining an \emph{evaluation context} We can formalize this by defining an \emph{evaluation context}
$\evCtx[\bullet]$, and saying $M$ is \emph{incorrectly flagged} $\evCtx[\bullet]$, and saying $M$ is \emph{incorrectly flagged}
@ -309,8 +307,7 @@ Like every active software community, Roblox developers share code
with one another constantly. First- and third-party developers alike with one another constantly. First- and third-party developers alike
frequently share entire software packages written in Luau. To add to frequently share entire software packages written in Luau. To add to
this, many Roblox games are authored not by just one developer, but a this, many Roblox games are authored not by just one developer, but a
whole team. team.
It is therefore crucial that we offer first-class support for mixing It is therefore crucial that we offer first-class support for mixing
code written in strict and nonstrict modes. code written in strict and nonstrict modes.