Hacker News new | past | comments | ask | show | jobs | submit login

Yeah! So you know that read:T call that you have implemented in Scala?

You know that it could produce a different result on consecutive calls, right? Because the notion of a mutex/lock doesn’t exist in Math.

Mathematics doesn’t allow that, because it is not a “pure function”.

https://en.wikipedia.org/wiki/Pure_function

Non-determinism is the norm in distributed systems.

e.g any networked Turing machine.




You seem to imply that there's no mathematical model/theory of non-deterministic/distributed systems. Surely you don't believe that?


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


> That is why Haskell's lazy evaluation leaks time.

Could you maybe illustrate this with an example?


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 ).

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/haskell/lazy.html


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..?).


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'.




Consider applying for YC's Spring batch! Applications are open till Feb 11.

Guidelines | FAQ | Lists | API | Security | Legal | Apply to YC | Contact

Search: