Hacker News new | ask | show | jobs
by ukj 2275 days ago
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'.