This paper discusses reasoning about IO operations in Haskell, Clean and C and compares the effect on ease of reasoning of
the different approaches taken to IO in these languages. An IO system model is built using VDM and is used to prove a basic
property of a program written in each of the three languages. We tentatively draw the conclusions that functional languages
are easier to reason about and that Monads can make the reasoning process slightly more difficult, but note that much future
work is needed.