Message Safety in Dart
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 OctDisplayed time zone: Eastern Time (US & Canada) change
10:30 - 12:00
Session 2, Formalization, Semantics, and Static AnalysisDLS at Grand Station 3
|A Formalization of Typed Lua|
Andre Murbach Maidl PUCPR, Fabio Mascarenhas UFRJ, Roberto Ierusalimschy PUC-RioMedia Attached
|Gradual Certified Programming in Coq|
Éric Tanter University of Chile, Chile, Nicolas Tabareau Inria
|Message Safety in Dart|
Erik Ernst , Mathias Schwarz Uber Aarhus, Fabio Strocco Aarhus University, Denmark, Anders Møller Aarhus University
|Control-Flow Analysis of Dynamic Languages via Pointer Analysis|
Steven Lyde , Matthew Might University of Utah, USA, William E. Byrd