Language Design Meets Verifying Compilers (Keynote)
Author(s). David J. Pearce.
Venue. In Proceedings of the Conference on Generative Programming: Concepts and Experiences, pages 104--123, 2022. ©ACM
Abstract.
The dream of developing compilers that automatically verify whether or not programs meet their specifications remains an ongoing challenge. Such ``verifying compilers’’ are (finally) on the verge of entering mainstream software development. This is partly due to advancements made over the last few decades, but also to the increasingly significant and complex role software plays in the modern world. As computer scientists, we should encourage this transition and help relegate many forms of software error to the history books. One way of increasing adoption is to design languages around these tools which look, on the surface, like regular programming languages. That is, to seamlessly integrate specification and verification and offer something that, for the everyday programmer, appears as nothing more than glorified type checking. This requires, amongst other things, careful consideration as to which language features mesh well with verification, and which do not. The design space here is interesting and subtle, but has been largely overlooked. In this talk, I will attempt to shed light on this murky area by contrasting the choices made in two existing languages: Dafny and Whiley.