SPLASH 2022
Mon 5 - Sat 10 December 2022 Auckland, New Zealand

An object under initialization does not fulfill its class specification yet and can be unsafe to
use as it may have uninitialized fields. It can sometimes be useful to call methods on such a
partially initialized object in order to compute a complex initial value, or to let the object
escape its constructor in order to create mutually recursive objects. However, inadvertent usage
of uninitialized fields can lead to run-time crashes. Those subtle programming errors are not
statically detected by most modern compilers.

While many other features of object-oriented programming languages have been thoroughly studied
over the years, object initialization lacks a simple, systematic, and principled
treatment. Building on the insights of previous work, we identify a set of four core principles
for safe initialization: monotonicity, authority, stackability, and scopability. We capture the
essence of the principles with a minimal calculus, Celsius, and show that the principles give rise
to a practical initialization system that strikes a balance between expressiveness and
simplicity. The meta-theory of the system is entirely mechanized using the Coq proof assistant. We
believe that our approach based on well-identified core principles sheds new light on the
underlying mechanisms ensuring safety and could serve as a basis for language design when faced
with similar challenges.