Message safety in Dart

- We present a core calculus of Dart, explaining its type system and the causes of unsoundness.
- A notion of message-safe programs is defined, which provides a natural level between dynamic and static typing.
- A soundness theorem is presented, stating that message-safe programs do not cause message-not-understood errors in checked mode execution.
- We report on initial experimental results that support the use of message safety in software development.

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.