Philipp Kant
physicist and functional programmer
Philipp started his career in theoretical particle physics, doing research on Higgs Bosons, supersymmetry, and top quarks. As a postdoc, he stumbled upon Haskell, and liked it well enough to eventually switch to software development. He now works at IOHK, where he sits at the interface between research and development. His team is collaborating with scientists to turn their research into specifications, prototypes, and working code.
Fusing Flexibility with Formality: Practical Experience with Agile Formal Methods in Large-Scale Functional Programming
Agile software development and Formal Methods are traditionally seen as being in conflict. From an Agile perspective, there is pressure to deliver quickly, building vertical prototypes and doing many iterations / sprints, refining the requirements; from a Formal Methods perspective, there is pressure to deliver correctly and any change in requirements often necessitates changes in the formal specification and might even impact all arguments of correctness.
These two goals are often discordant. In this paper, we argue that given the right attitudes on both sides, it is possible to fuse good practices from formal methods and agile software engineering to deliver software that is simultaneously reliable, effective, testable, and that can also be delivered rapidly.
This suggests a new lightweight software engineering methodology, that is inspired by and exploits appropriate formal methods, while also providing the benefits of agile software development. Our methodology is informed and motivated by practical experience. We have devised and adapted it in the light of experience in delivering a large-scale software system that needs to meet complex real-world requirements: the Cardano crypto-currency.
Crypto-Currencies is a rather new application area for which no clear engineering habit exists, so it is a fitting domain for agile methods. At the same time, there is a lot of real monetary value at stake, making it a good fit for using formal methods to ensure high quality and correctness. The paper reports on the issues that have been faced and overcome, and provides a number of real-world lessons that can be used in similar situations.
Video ←Back
