一句话：提出安全对象初始化的四条核心原则，并以最小演算 Celsius 及 Coq 机器化证明实现兼具表达力与简洁性的初始化系统。
对象在初始化过程中可能尚未满足类规约，字段未初始化，若此时调用方法或让对象逸出构造函数，易导致运行时崩溃；现代编译器大多无法静态检测此类错误。面向对象语言的其他特性已有深入研究，但对象初始化仍缺乏简单、系统且原则化的处理。本文在已有工作洞见基础上，提炼出安全初始化的四条核心原则：单调性、权限、可栈化与可作用域化，并以最小演算 Celsius 形式化这些原则。作者证明该原则体系可导出一个实用的初始化系统，在表达力与简洁性之间取得平衡；整个元理论均使用 Coq 证明助手机器化验证。该框架为语言设计者在面对类似安全挑战时提供了原则化基础。
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.
@article{paperbot1466,
title = {A conceptual framework for safe object initialization: a principled and mechanized soundness proof of the Celsius model},
author = {Clément Blaudeau and Fengyun Liu},
journal = {Proceedings of the ACM on Programming Languages},
volume = {6},
number = {OOPSLA2},
year = {2022},
doi = {10.1145/3563314}
}