FUNARCH '25: Proceedings of the 3rd ACM SIGPLAN International Workshop on Functional Software Architecture

The formal verification of an optimising compiler for a realistic programming language is no small task. Most verification efforts develop the compiler and its correctness proof hand in hand. Unfortunately, this approach is less suitable for today’s constantly evolving community-developed open-source compilers and languages. This paper discusses an alternative approach to high-assurance compilers, where a separate certifier uses translation validation to assess and certify the correctness of each individual compiler run. It also demonstrates that an incremental, layered architecture for the certifier improves assurance step-by-step and may be developed largely independently from the constantly changing main compiler code base. This approach to compiler correctness is practical, as witnessed by the development of a certifier for the deployed, in-production compiler for the Plinth smart contract language. Furthermore, this paper demonstrates that the use of functional languages in the compiler and proof assistant has a clear benefit: it becomes straightforward to integrate the certifier as an additional check in the compiler itself, leveraging the the Rocq prover’s program extraction.

Since 2019, the International Software Architecture Qualification board has featured a three-day curriculum for Functional Software Architecture. We have taught more than 30 trainings based on this curriculum, mostly to audiences with little or no exposure to functional programming. This paper reports on our experience, and how content and delivery of the training has evolved over the past four years.

Functional paradigms for user-interface (UI) programming have undergone significant evolution, from early stream-based approaches, monad-based toolkits mimicking OO practice to modern model-view-update frameworks. Changing from the classic Model-View-Controller pattern to functional approaches drastically reduces coupling and improves maintainability and testability. On the other hand, achieving good modularity with functional approaches is an ongoing challenge. This paper traces the evolution of functional UI toolkits along with the architectural implications of their designs---including two of our own---summarizes the current state of the art and discusses remaining issues.