Unlike traditional static type checking, the type system in the Dart programming language is unsound by design, even for fully annotated programs. The rationale has been that this allows compile-time detection of likely errors and enables code completion in integrated development environments, without being restrictive on programmers.

Despite unsoundness, judicious use of type annotations can ensure useful properties of the runtime behavior of Dart programs. We present a formal model of a core of Dart with a focus on its type system, which allows us to elucidate the causes of unsoundness. Our main contribution is a characterization of message-safe programs and a theorem stating that such programs will never encounter ‘message not understood’ errors at runtime. Message safety is less restrictive than traditional type soundness, and we argue that it forms a natural intermediate point between dynamically typed and statically typed Dart programs.

Tue 27 Oct

10:30 - 12:00: DLS - Session 2, Formalization, Semantics, and Static Analysis at Grand Station 3
dls201510:30 - 10:52
Media Attached
dls201510:52 - 11:15
Éric TanterUniversity of Chile, Chile, Nicolas TabareauInria
dls201511:15 - 11:37
Erik Ernst, Mathias SchwarzUber Aarhus, Fabio StroccoAarhus University, Denmark, Anders MøllerAarhus University
dls201511:37 - 12:00
Steven Lyde, Matthew MightUniversity of Utah, USA, William E. Byrd