BOB 2025

Against the (formal) method?
2025-03-14 , Talks B
Language: English

Formal methods are very often touted as a necessary evolution of software development to cope with increasing complexity, risks, and challenges. This is especially true in functional programmers' circles, as there's historically a strong link between functional programming languages and formalisation of computing. After all, if software engineers really want to be considered as "true" engineers like mechanical or nuclear engineers, they will need to embrace formalisation and root their practices and tools in solid mathematical foundations.
But one can ask the question: is this narrative true? Is it necessary for software development to come of age and embrace formal methods? And, perhaps more importantly, is it desirable?
Based on my experience developing software over the past 30 years, in a wide array of environments, some of which even using formal methods, and some theoretical, epistemological and philosophical references, I try to answer those questions in a more nuanced way.
This presentation puts formal methods (FM) in perspective within the broader domain of software development, as yet another tool to deliver value. I shall present my experience working with FM, identify various shortcomings and issues of FM in the software development lifecycle, and suggest ways to mitigate those issues in order to help teams benefit the most from FM.


3-5 take-home ideas:
  • FM are often smart and cool, but this coolness has a price tag your team or organisation might not be able to pay: Be careful what you wish for!
  • FM tooling does not always play well with typical software development workflow, but there are ways to make them nicer citizens:
  • FM can be intimidating and is often presented as an all-or-nothing solution, but it does not have to be and it's actually much better to start small: Focus your efforts on things that matter

Arnaud has been developing software and helping teams develop software for nearly three decades, in various technologies, contexts and roles. He is interested in everything software-related with a peculiar passion for strongly-typed functional programming.