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