User settings, Lamport clocks and lightweight formal methods
jakub-m.github.io
jakub-m.github.io
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
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
Yes, you are right. To rephrase, you say that a browser could first increment its clock to the value larger that the backends, and then synchronize and "win" with the backend, setting the backend value to some bogus "none".
I'd say that it's "fine" in a way that the browser and the backend agree to "something" and are in sync. The case we wanted to prevent was that the browser and the backed hold different values and cannot agree which value to converge to.
But perhaps you wanted something that actually handles the conflicts, like for a list of subscribers to an event. In that case you would want to use a vector clock instead of a lamport timestamp, and then when neither clock dominates the other (aka when they are tied), you take both sets and merge them. This is an incomplete outline of the “add-wins set” CRDT.
I wish CRDTs were more mainstream :)
For settings where we can more intelligently handle conflicts (e.g. sets), we don't need the timestamps, because we can take advantage of vector clocks instead.
forAll (x: Int) { assert(x.abs >= 0) }
Whilst such approaches don't let us prove such statements (except for exhaustively checking small input spaces, e.g. `forAll (x: Boolean, y: Boolean) ...` only needs four tests), I find it just as easy as normal unit testing, and far less effort than formal proofs (e.g. using Coq or Agda)
(FYI that property is in fact false, since it doesn't hold for -2147483648; ScalaCheck's random generators are biased towards such "problematic" values, e.g. -inf, NaN, etc., so it usually find such things)
"I get paid for code that works, not for tests, so my philosophy is to test as little as possible to reach a given level of confidence" — Kent Beck
And as a seller of programming books, he increases his target audience by excluding the small percentage of mathematically literate programmers and appealing to the majority who find logic intimidating.
His work has directly shaped how many distributed systems reach consensus. Including recent projects like Solana. Also check out VDF and proof of history.
Ingenious!
This is covered in the classic "Time, Clocks" paper (https://www.microsoft.com/en-us/research/uploads/prod/2016/1...). If you read exactly one distributed systems paper in your life, it should probably be this one.