Input from an arbitrary source (i.e. without referential transparency) implies that there can be no equational reasoning, almost by definition. This is kind of

Input from an arbitrary source (i.e. without referential transparency) implies that there can be no equational reasoning, almost by definition. This is kind of the case for IO in Haskell[0], but for subprograms/procedures/functions I tend to find it an absolutely essential property, both in terms of reasoning and in terms of testability. For example, it's the whole reason that QuickCheck works. [0] Modeling IO as a World->World function doesn't quite work.