Unfortunately, that “truth” still resists a denotative representation:
(page 353 of 600)
During the 1960s, several researchers began work on proving things about programs. […]
Several difficult problems emerged from this work. One was the problem of specification : before one can prove that a program is correct, one must specify the meaning of “correct”, formally and
Researchers began to analyze why it is often harder to prove things about programs written in traditional languages than it is to prove theorems about mathematics. Two aspects of traditional languages emerged as sources of trouble because they are very difficult to model in a mathematical system: mutability and sequencing.
The Anatomy of Programming Languages (1993)
…but as I noted earlier , it’s mutation which is the actual mathematical misfit.
Some here (including me) would beg to differ:
(http://discourse.haskell.org/t/haskell-vs-purescript-mmmm-just-bad-tech-journalism/7093/14)
I spent decades programming in procedural languages, where I had to continually think about order of evaluation. It sucks.
As further evidence of this, consider the type ST s a. Just like IO a, it facilitates mutation and thus relies on sequencing - surely it must be just as irritating!
But of the two, only IO a seems to attract all the criticism e.g:
…a curious dichotomy.
…more precisely, strict functional and imperative programming:
In lazy functional languages like Haskell or Miranda, evaluation order is dynamically determined, so can be immensely difficult to predict. If such languages obtained imperative actions as side-effects of evaluation then serious reasoning difficulties would result. Determining which side effects are to be performed, and worse, in which order, would rely on determining the exact order of evaluation - the very thing that laziness tends to hide! Consequently lazy evaluation and side effects do not mix.
Lazy Imperative Programming (1993)
…which is why Haskell has the type ST s a - see State in Haskell (mentioned here ) for the details.