[joel_ms]

Thank you!

I was more wondering how time leaks and laziness relates to denotational vs operational semantics? I couldn't find anything about either in the links (they seem to be general descriptions of haskell and laziness..?).

[ukj]

Trivially. For any given system 'safety' is an operational concept, not a denotational one.

You can't formalize the notion of 'safety' let alone prove (in the Mathematical sense) that your code has it without examining its runtime behaviour.

In the words of Donald Knuth: Beware of bugs in the above code; I have only proved it correct, not tried it.

In one context lazy evaluation may be 'safe' - it another it may be 'dangerous' - the context in which this assertion is made is always about human needs and expectations, not mathematics.

With particular example being that lazy evaluation allows for side-channel attacks in cryptographic systems. That's undesirable - hence operationally 'unsafe'.