Practical Verification of a Free Monad Instance

Abstract

Formal verification of software is a largely underrepresented discipline in practice. While it is not the most accessible topic, efforts are made to bridge the gap between theory and practice. One tool conceived for this exact purpose is agda2hs, a tool intended to allow developers to create their programs correct-by-design. A program written a proof assistant language Agda, along with the proof of its correctness, can be translated to the readable Haskell equivalent, retaining only the functionally relevant aspects and leaving the proof related aspects of the code behind. This paper describes research done into the current abilities of agda2hs on the use case of verifying properties of free monads, a higher order type with potential for use in implementation of domain specific languages and purely functional and modular handling of effects. In order to represent an aspect of the type in a general way I used containers, a uniform way of representing types that store data. This led me to a limitation of agda2hs: while the tool in its current state can only handle direct translations from a common subset of the two languages, in order to translate my definition of the data type I needed a more fine grained control of the translation process which the tool could not provide.