Lambda the Ultimate

inactiveTopic I/O in Three Programming Paradigms
started 3/17/2003; 8:54:37 AM - last post 3/17/2003; 8:54:37 AM
Isaac Gouy - I/O in Three Programming Paradigms  blueArrow
3/17/2003; 8:54:37 AM (reads: 226, responses: 0)
Comparing Proofs about I/O in Three Programming Paradigms

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?

For an answer, we need to read: Proving Correctness of Programs with I/O --- A Paradigm Comparison