Replaying immutable events in a deterministic order doesn't fit so well with Automerge; Automerge is more designed for apps where you can represent the mutable state of your application as an Automerge doc. https://livestore.dev/ might be a better fit for you.
Thank you! To your point about industrial use, yes – this is interesting. For example, Actyx makes a software system for coordination within a factory floor, and Ditto performs sync between devices of cabin crew on an aircraft. These are nice examples of industrial local-first systems.
I agree that for most engineers, getting into formal proof is intimidatingly hard and perhaps not a good use of time, because lighter-weight specification languages and model-checking can help develop a good understanding of a system's behaviour with a much lower time investment.
But the intended audience for this post was not engineers working on production systems; it was intended for researchers studying distributed algorithms (e.g. consensus algorithms), and researchers who already know proof assistants and want to know how to use their skills to verify distributed algorithms. Note that this post appeared on a blog called "Machine Logic", not "Practical Distributed Systems Engineering"!
I have personally got a lot of value out of formal verification because the distributed algorithms I work on (CRDTs) are sometimes so subtle that without a proof of correctness, I simply don't believe that they are correct. I have several times developed algorithms that I believed to be correct, only later to find out that I was wrong. Here's a case study of one such example: https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-969.pdf
For people like myself, who are designing such algorithms, I believe that formal proof is worth the effort. But most people are not in this situation.
Hi, one of the authors here. You're right that in order to ensure that you won't receive timestamps lower than some threshold, you need to know all the nodes in the system, and you need to hear from all of them (if even just one node is unreachable, that will be enough to hold up the process). That's quite a big assumption to make, but unfortunately there doesn't really seem to be a good way around it. Lots of CRDT algorithms have this problem of requiring causal stability for garbage collection.
Using a consensus protocol is possible, and would have the advantage that it only requires communication with a quorum (typically a majority of nodes), rather than all nodes. However, it has the downside that now a node cannot generate timestamps independently any more — generating a timestamp would then also require a round trip to a quorum, making the algorithm a lot more expensive.
Martin here. I cited your paper in the related work section. It's a good start, but it does not cover everything that's required to achieve BFT — in particular, the issue that an operation may be valid in some contexts and invalid in others, and all correct nodes need to agree on whether an operation is valid or not.
If you have more details on the caveats you have discovered, it would be great if you could write them up so that others can learn from your experience!
Hello, Martin here :) I use the Paper app (https://wetransfer.com/paper) on an iPad, then transfer the images to a computer, do a little post-processing in Gimp and ImageMagick, and then drop the images into PowerPoint. You might be able to present directly from the Paper app, but it's more designed for drawing than for presenting.
Interesting idea, but the devil is in the details. Especially two concurrent moves of partially overlapping ranges of characters is a tricky case to handle, and it is not obvious to me how your scheme would deal with this.
Another fun case is two concurrent range moves in which the destination of the first move falls within the second move's source range, and the destination of the second move falls within the first move's source range. How do you handle this?
I expect that any algorithm solving this problem will need a formal proof of correctness, because it's very easy to miss edge cases when using informal reasoning.
Just for the record, I was already aware of GUN previously, and think it is a good project to include in the list. We had just forgotten about it when putting together this list of links. I guess I don't check HN all that often. ;)
I just looked up my own O'Reilly book on ebooks.com.
http://www.ebooks.com/95729334/designing-data-intensive-appl...
I can't see anything about DRM on the page, but under "supported devices" it says "e-readers with Adobe Digital Editions installed". Isn't that DRM enforcement software? Could you clarify please?
I only have the blog post to go by, and don't have first-hand information. It seems possible to me that a few packets could indeed be delayed by 90 seconds, perhaps stuck in a switch buffer somewhere, although this would be a small number of packets since those buffers are not very big.
However, yes, I was thinking about the network stack as a whole. Any kind of retries, e.g. TCP retransmission on timeout, effectively turns packet loss into packet delay (within certain bounds). Thus, even if you have a network interruption ("partition") and all packets are dropped, it could happen that after the interruption is fixed, a node receives packets that were sent before or during the interruption. For this reason, I find it helpful to think of it as delay, not just packet loss.
The FLP result (Fischer, Lynch, Paterson) shows that consensus cannot reliably be solved in an asynchronous system (if you do not make any timing assumptions) if one or more processes can fail. The impossibility result shows that any consensus algorithm in such a system will have executions in which it waits forever and never makes a decision, which breaks the liveness property of consensus.
However, if you do allow some timing assumptions — just enough to measure a timeout, nothing more — then consensus becomes possible. In this case, the timeout is known as an "unreliable failure detector". See Chandra and Toueg's paper for details.
In a good algorithm, the safety properties do not depend on timing, only the liveness properties do. Rather than "consensus being impossible" perhaps it would be clearer to say "consensus may never terminate" in an asynchronous system. But "consensus impossible" is the standard way of phrasing this issue in the distributed systems literature.
There are some pointers to better terminology at the end of the post — e.g. I like Terry's session guarantees (read-your-writes, monotonic reads, etc) — but they too only cover a small subset of the design space.
In the end, this stuff is still evolving, and we simply don't yet know the best way of describing things. I wouldn't want to propose some alternative classification scheme that would be no better than the one it replaces. But I do want to encourage people to be precise and thoughtful with the terminology they use.
My beef with CAP is not that it's so broad, but that it's so narrow. It actually only proves a fairly small class of systems as impossible, and it's kinda obvious. Literature going back to the 1970s suggests that the trade-off was well known back then -- just not under such a catchy name.
Impossibility results are great, but misinterpreting them and using them to argue stuff to which they simply don't apply is not so great.