An often cited advantage of functional programming languages is that they are supposed to be easier to reason about than imperative languages... For a long time, a major disadvantage of functional programming languages was their inability to adequately handle features where side-effects are an intrinsic component, such as file or other I/O operations... two methodologies have
emerged in the last decade to combine the side-effect world of I/O with the referentially transparent world of functional programming, namely the uniqueness type system of the programming language Clean and the use of monads in the Haskell language.
However, as a consequence of these developments, functional programs written in these languages now look very like imperative programs — as evidenced by sample programs appearing later in this paper. This immediately raises concerns about the relative ease of reasoning about such programs, when compared to similar programs done in an imperative style.
Question: Has the technical machinery necessary to handle I/O in pure functional languages, led to a situation where correctness proofs have the same diffculty as those found in imperative programs?
I/O in Three Programming Paradigms
