Teaching and researching formal semantics of functional programming languages, while looking for ways of solving complex, practical problems with formal methods in order to create trustworthy tools for the Erlang programmer. Truly enthusiastic about formally verified static analysis and code refactoring.
Ensuring program correctness (particularly in concurrent systems) is a complex challenge. Subtle bugs often arise from unexpected interactions or code changes and may go undetected until they cause failures in production. Formal methods help address these challenges by providing mathematically precise definitions and proofs of program behaviour. This talk focuses on Core Erlang, an intermediate language used within the Erlang compiler, and its precise implementation using the Coq/Rocq proof management system.
We explore practical tools built on this foundation, such as verifying program correctness and ensuring that refactorings and optimisations preserve behaviour without relying on testing. We also present a formally based interpreter for Erlang that validates our definitions against the behaviour of Erlang/OTP. Beyond serving as a reference implementation, our interpreter also enables systematic exploration of possible schedulings in concurrent programs, aiding developers in code comprehension. Our formal model also supports a long-term goal: developing a verified Erlang compiler free from miscompilation issues.
Key Takeaways:
Target Audience: