Pretty printers make trade-offs between the expressiveness of their pretty printing language, the optimality objective that they minimize when choosing between different ways to lay out a document, and the performance of their algorithm. This paper presents a new pretty printer, Π e , that is strictly more expressive than all pretty printers in the literature and provably minimizes an optimality objective. Furthermore, the time complexity of Π e is better than many existing pretty printers. When choosing among different ways to lay out a document, Π e consults a user-supplied cost factory , which determines the optimality objective, giving Π e a unique degree of flexibility. We use the Lean theorem prover to verify the correctness (validity and optimality) of Π e , and implement Π e concretely as a pretty printer that we call PrettyExpressive. To evaluate our pretty printer against others, we develop a formal framework for reasoning about the expressiveness of pretty printing languages, and survey pretty printers in the literature, comparing their expressiveness, optimality, worst-case time complexity, and practical running time. Our evaluation shows that PrettyExpressive is efficient and effective at producing optimal layouts. PrettyExpressive has also seen real-world adoption: it serves as a foundation of a code formatter for Racket.

@article{paperbot1848,
  title = {A Pretty Expressive Printer},
  author = {Sorawee Porncharoenwase and Justin Pombrio and Emina Torlak},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {7},
  number = {OOPSLA2},
  year = {2023},
  doi = {10.1145/3622837}
}