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.