Against the (formal) method?

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.

Arnaud Bailly

‘@abailly.bsky.social

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.