[HN Gopher] User settings, Lamport clocks and lightweight formal...
       ___________________________________________________________________
        
       User settings, Lamport clocks and lightweight formal methods
        
       Author : iforgetlogins01
       Score  : 24 points
       Date   : 2022-07-20 20:15 UTC (2 hours ago)
        
 (HTM) web link (jakub-m.github.io)
 (TXT) w3m dump (jakub-m.github.io)
        
       | danuker wrote:
       | Can't help but think that this "logical clock" doesn't care
       | simultaneity is relative.
       | 
       | Ingenious!
        
       | User23 wrote:
       | Interesting. Incidentally, I would claim that TDD done properly
       | is in fact a lightweight formal method. It helps to be conversant
       | with some kind of formal semantics, but you can definitely play a
       | bit fast and loose by treating your tests as a lightweight
       | specification. In that case any formal properties I want the code
       | to have that can't practically be expressed in the test is
       | included in a comment on the test. Also, fuzzing is a way to
       | narrow that gap further.
        
         | subleq wrote:
         | A failing test can only prove the existence of a bug. A passing
         | test can not prove that there are no bugs.
        
       | TheTaytay wrote:
       | Thanks for the article! I love lamport clocks, and the
       | lightweight methods are cool.
       | 
       | I read through the article a couple of times, and was unsure
       | about something: When the browser resets, it does not appear to
       | copy down the current state and clock value from the server,
       | right? I'm basing that on this from the article:
       | The browser resets, all the state is dropped.       browser:
       | settings: none, clock: 0       backend: settings: foo, clock: 2
       | 
       | I don't think that lamport clocks can be compared if they are not
       | representing any concept of causality or knowledge, right? This
       | implementation appears to be two separate integers (one for the
       | client and one for the server), with no guarantee as to their
       | ability to communicate with each other. One bug you discovered
       | was that the server might have a value 2, and the client might
       | have a value 2, but they would disagree on the state that value
       | "2" referred to. A bug indeed! Your fix was to handle the case
       | where the client and server tied. However, I was left wondering:
       | What about the case where the knowledge of the client is higher
       | than the server, but the server still should not trust it? What
       | if, in your example step 4, the client had made 3 changes without
       | the ability to sync with the server? It would be this:
       | The user changes the settings three times, but this time the
       | state is not propagated to the backend (e.g. due to network
       | hiccups).       browser: settings: none, clock: 3       backend:
       | settings: foo, clock: 2
       | 
       | In that case, by the time the client talks to the server, the
       | server would think that the client had "won", but the fact that
       | the client had a clock value of "3" would be meaningless, right?
       | Wouldn't you still want the server to win in this case?
        
       ___________________________________________________________________
       (page generated 2022-07-20 23:00 UTC)