Many mainstream programming languages are dynamically typed. This allows
for rapid software development and programming flexibility because it gives
programmers the freedom to use powerful programming patterns that are not
allowed in statically typed programming languages. Nevertheless, this freedom
does not come without drawbacks: static bugs detection, IDE support, and
compiler optimization techniques are harder to implement. In the last decades,
the research literature and mainstream programming languages have been
aiming to reach a trade-off between statically typed and dynamically typed
languages.
We investigate the trade-off, focusing on the area of optional typing, which
allows programmers to choose when to use static type checking in parts of pro-
grams. Our primary focus is Dart, an optionally typed programming language
with a type system that is unsound by design. What makes Dart interesting
from a research point of view is that the static type system combines optional
typing with nominal typing using subtyping rules that make the type system
unsound even for fully annotated programs.
This dissertation contains three main contributions. We first show a for-
mal model in Coq of a subset of the Dart type system and operational se-
mantics. We prove in Coq that natural restrictions of the Dart type system
guarantee the absence of runtime type errors caused by calls to missing meth-
ods and functions, without going all the way to full soundness. Our second
main contribution concerns the design of a type safety analysis for the full
Dart language, and experimental evaluations showing that the algorithm can
be successfully applied to real-world programs. Our third main contribution
consists of experimentally evaluating the benefits provided by each source of
unsoundness in the Dart type system.