5 ms·

I am implying that Mathematical semantics are broken/incomplete. Mathematics uses denotational semantics. It implies pass by-value and pass-by-reference are eq

by ukj 7y ago

I am implying that Mathematical semantics are broken/incomplete. Mathematics uses denotational semantics. It implies pass by-value and pass-by-reference are equivalent. They are in theory, they aren't in practice. That is why Haskell's lazy evaluation leaks time. Engineers/physicists intuitively rely at least on operational semantics. It's a higher order logic, and since Linear Logic time is localized. https://ncatlab.org/nlab/show/Geometry+of+Interaction https://ncatlab.org/nlab/show/Geometry+of+Interaction

cannabis_sam 7y ago
> That is why Haskell's lazy evaluation leaks time. Could you maybe illustrate this with an example?
- ukj 7y ago
  So as a brief summary: laziness leaks time. Whether that's a good or a bad thing depends on what you want/need. It may be a bad thing if you are doing cryptography because time leaks allow side-channel attacks ( https://en.wikipedia.org/wiki/Timing_attack https://en.wikipedia.org/wiki/Timing_attack ). As with all philosophical squabbles - there are arguments for each side. It's up to you to make up your mind based on your particular use-case. And so in context of crypto + Haskell, have a look at these two posts: https://crypto.stanford.edu/~blynn/c/haskell.html https://crypto.stanford.edu/~blynn/c/haskell.html https://crypto.stanford.edu/~blynn/haskell/lazy.html https://crypto.stanford.edu/~blynn/haskell/lazy.html
  - joel_ms 7y ago
    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 7y 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'.

by ukj 7y ago

cannabis_sam 7y ago

> That is why Haskell's lazy evaluation leaks time. Could you maybe illustrate this with an example?

ukj 7y ago
So as a brief summary: laziness leaks time. Whether that's a good or a bad thing depends on what you want/need. It may be a bad thing if you are doing cryptography because time leaks allow side-channel attacks ( https://en.wikipedia.org/wiki/Timing_attack https://en.wikipedia.org/wiki/Timing_attack ). As with all philosophical squabbles - there are arguments for each side. It's up to you to make up your mind based on your particular use-case. And so in context of crypto + Haskell, have a look at these two posts: https://crypto.stanford.edu/~blynn/c/haskell.html https://crypto.stanford.edu/~blynn/c/haskell.html https://crypto.stanford.edu/~blynn/haskell/lazy.html https://crypto.stanford.edu/~blynn/haskell/lazy.html
- joel_ms 7y ago
  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 7y 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'.