Composite Replicated Data Types: eventually consistent libraries as non-leaky abstractions

Composite Replicated Data Types
Alexey Gotsman and Hongseok Yang
2015

Modern large-scale distributed systems often rely on eventually consistent replicated stores, which achieve scalability in exchange for providing weak semantic guarantees. To compensate for this weakness, researchers have proposed various abstractions for programming on eventual consistency, such as replicated data types for resolving conflicting updates at different replicas and weak forms of transactions for maintaining relationships among objects. However, the subtle semantics of these abstractions makes using them correctly far from trivial.

To address this challenge, we propose composite replicated data types, which formalise a common way of organising applications on top of eventually consistent stores. Similarly to a class or an abstract data type, a composite data type encapsulates objects of replicated data types and operations used to access them, implemented using transactions. We develop a method for reasoning about programs with composite data types that reflects their modularity: the method allows abstracting away the internals of composite data type implementations when reasoning about their clients. We express the method as a denotational semantics for a programming language with composite data types. We demonstrate the effectiveness of our semantics by applying it to verify subtle data type examples and prove that it is sound and complete with respect to a standard non-compositional semantics

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Sorry, but useless without a performance analysis

Since the problem of replicated stores can be roughly described as: we can only provide weak guarantees due to performance issues, I can't care about this study without a performance analysis.

Solves the wrong question.

Unhappy

I am not very happy with the form of your remark. I'm exposing work that I found interesting, and you offer a counter-opinion, that is actually a question (are there experimental results that eventual consistency is performance-critical?) in a form that is (1) without object in my opinion (2) rude and disrespectful of the work presented.

Let me substantiate point (1) because I think (2) is obvious. It is a fair question to ask whether eventual-consistency-like restrictions are really required in practical applications. I think, but I'm not an expert in this area, there is ample evidence that it is that you could find by browsing the references of this article. Note however that those weaker properties are often motivated by the problem of avaibility and resilience to network partitions rather than performance per se. The question is fair, but it is unfair to expect this article to perform and present this analysis and to criticize it solely for not doing that.

This article evidently assumes (rightly, I believe) that the analysis has been done, and builds on top of the assumed need to modularly program eventually-consistent or casually-consistent systems. I think it is an interesting and important question, and furthermore it is evidently a language-oriented question, which makes it highly relevant to LtU.

P.S.: the but-last time I posted an article on the LtU frontpage, one of the article's authors came by (I assume, to interact and eventually answer interesting questions or remarks arising from the discussion) and was evidently put off by the tone of the first comment in the discussion -- which was weird, but much less unpleasant than what marco just produced. I will not have my contributions to this website turn into a bullying platform.

Philosophy

I fully appreciate that people will a degree in philosophy do that, produce philosophical work.

If there is work which does the performance analysis right, than they should have lifted that.

Who is this helping?

I haven't looked at the paper yet so I won't address the substance of your gripe, but I've had plenty of times where my reaction to a paper posted to the site is "surely this isn't the best way to go about this". Several of those have resulted in LtU posts that I look back at and cringe a little. It's obviously a good idea to ask "who is this helping?" Are you seeking clarification for yourself or providing constructive criticism and is your post appropriate for that purpose? And remember that the author may reply.

Life is short. In a hundred years everybody here will be dead.

I haven't been rude. I've dismissed the paper with an argument. A polite argument too.

The response was an ad-hominem.

Adults can take criticism.

No worries

I was responding more to your second comment, which seemed mostly content free, than to your first, but I guess you were just goading gasche. I don't think you've been particularly polite here but you didn't offend me. I do suspect that perceived impoliteness keeps away a certain class of posters. Though probably not as often as perceived dumbness of a discussion.

Not Worried

Yah, well. I don't like theory for the sake of theory. As it stands, I see two problems with the paper:

  1. Solves the wrong problem. Performance is key.
  2. Solves the problem in the wrong manner. Denotational semantics is overkill.

I don't mind being a party pooper. If there's something I missed, people can explain it.

Performance of a database is

Performance of a database is not the only reason to like CRDTs. When you have a multi user application and a user does an operation you often don't want to wait to display the result until the server has acknowledged that the operation succeeded, you want to display the results immediately. This means that clients can temporarily go out of sync, and when they go out of sync in conflicting ways you need to resolve the conflict somehow. That is exactly the problem that CRDTs tackle.

from another curmudgeon $0.02

I don't understand how people don't have thicker skin and how anybody can "blame the user", at least in cases where a technical point is made. But that's just me. And marco. I guess. Yes, there is a range of behaviour and no we don't want LtU to be only jerky talk, but sheesh, can't anybody take a critique?! Are people who publish really that wimpy? What has 'civilization' come to?

It would be one thing if marco had done it ad hominem or used four letter english curse words. But to me just being brief and to the point isn't insulting. It might be *wrong*, he might be *wrong*, but then that's his problem for looking like a doofus.

Yes, if the community is not replying to the thread and there's only one comment and it looks "mean" to some people I can see how one might argue that overall looks bad for LtU. To me the answer is more that the original poster must always be on duty to try to take whatever is said and reply to it in a way that makes it clear e.g. to any visiting author that it doesn't represent LtU's attitude across the board. But otherwise I guess to me the curt nature of the post is just that - curtness.

$0.02

p.s. if the back and forth on a topic with such a poster ends up being clearly pointless after 1 or 2 exchanges, then mark them in your own mind as a troll and ignore them. Most of the time I think the reason things stand out is when there isn't enough other discussion. In other words, w/out the ability to vote posts up/down, then we are stuck with the temporal posting nature of this drupal site.

It turns people off to posting

Telling the regulars here to have a thicker skin is missing the point that there experts in the field who may occasionally feel like dropping in to post insightful things. And if it looks like a brawl, they won't.

pick your lesser evil

Ok, hmmm.... I can see what you mean. But...sSo everybody involved in a "regular" discussion has to be namby-pamby nice all the time just in case some god decides they want to drop in?

Anyway, overall I think the whole thing could be better addressed through, of course, better UX and better technology: The comments could and maybe should be done more like Slashdot, Reddit, etc. so that things can hopefully sort of self-correct. (I know that much of an evolution isn't likely to happen any time soon, more is the pity. No, I don't have the time or smarts to volunteer to do it, either.)

I have a problem with this thread

I left myself a day to think about this, but I still find this thread hugely problematic.

marco's behavior is in clear violation of the LtU policies (or any rules that somehow requires to be respectful, such as the very first of the "core rules of Netiquette" cited in the LtU policies document). Other members have (rather weakly) reiterated that his behavior is problematic, yet marco seems (1) apparently unable to see any issue ("I haven't been rude. I've dismissed the paper with an argument. A polite argument too."; wow) and (2) unwilling to change his behavior in any way (I'm not even starting to consider that he could, you know, apologize for being rude), further insisting on being rude with a weird rationalization that this could be helpful ("If there's something I missed, people can explain it.").

I can stand rudeness directed against me -- although I would probably not participate much to discussions if I had to. What is unacceptable to me is that posting other people's work exposes them to extreme rudeness. I cannot serenely contribute stories to this website if I have to first wonder about the tolerance level of authors to abuse. (More than one author of interesting work would have a bad day if they read on a large-audience website that their work is "useless", "philosophical" and "wrong"). I should not have to worry about this (for example if LtU policies were respected), and this is the first time it is so bad (it was just cringey-level last time), but I cannot predict when it will happen again, or assume that it won't, given the unashamed acceptance of extreme rudeness in the present thread.

I will stop posting references to other people's work until I get reasons to trust that the work will be discussed in a respectful manner. Reasons could include promises by marco to stop being so disrespectful, or an agreement from whoever has moderation powers to remove such mildly-abusive comments (or silence their authors) in the future. The interest of active site members for behaving in a nice and respectful manner seems rather low, and I would understand if they decided not to do that (moderation is time-consuming and carries its own risks), but I will not participate to such an unpleasant environment.

So everybody involved in a "regular" discussion has to be namby-pamby nice all the time just in case

Yes.

nice vs. blunt

I'm torn here. Yes, I get that we should all have well-developed filters that prevent us from communicating our first uncouth thoughts that can create misunderstandings and hurt feelings. On the other hand, there are thoughts that should be communicated, often to simply have them corrected. I'm clearly aware of both sides.

In more well-polished forums (much of academia), negative thoughts can only be leveled passive aggressively since only that is acceptable. But that really is its own hell. In an ideal world, we would all go out and have beer together, generate some trust between us, and be able to talk bluntly without hurt feelings.

Unfortunately, none of you live in Beijing.

Expressing negativity

In more well-polished forums negative thoughts can only be leveled passive aggressively since only that is acceptable. But that really is its own hell.

I noticed this problem (the last time I attended an academic conference) and occasionally discuss it, but I have not yet found a best solution -- my personal tactic is to go talk to people and voice my potential criticisms directly but privately, and it is only a partial solution.

I am very happy to see constructive criticism and it motivates me to participate in discussions. Some of the criticism voiced in this thread is (a bit naive but) in a perfectly acceptable form. For example (citing macro again):

The denotational semantics look like overkill for this application. My first order approximation would be to express invariants through the type system, not derive a denotational semantics for it, and then show performance guarantees and the like.

This is a plausible opinion expressed in a way that I do not expect to be hurtful to anyone. (My first reaction to the presented work was, in fact, quite similar ("there is a type system in disguise"), but on further reflection I am not sure it would be simple to capture such trace properties into a type system.)

Compare it to the following remark that is equivalent in terms of content:

Yah, well. I don't like theory for the sake of theory. As it stands, I see two problems with the paper:
- Solves the wrong problem. Performance is key.
- Solves the problem in the wrong manner. Denotational semantics is overkill.

The former way to express criticism was acceptable (and it is not passive-agressive and can provoke further discussion), the second is not. I suppose it should be easy for most people to draw that line.

It is the unfiltered

It is the unfiltered thoughts that pop into your mind during a conversation that are more tricky. You provide a perfect example where (b) Marco expresses himself bluntly (his initial thoughts?) vs. (a) more constructively. We'd like to get to (a) without going through (b) but sometimes that doesn't happen: people just have differently developed internal censors as well as different levels where they get offended. You will draw lines differently from others, my filter is different from yours. A bit of tolerance is needed on both sides: accept that not everyone will express themselves in a way that you find acceptable, AND accept that not everyone will find what you have expressed as acceptable (and be non-defensive when told so). Barring that, just be very careful and walk on egg shells.

The PL community is not a "nice" place, especially if you are different. Bullies abound, and the real hurtful crap is not from unfiltered comments like this. There are plenty of cleaner forums, but they are either just boring or ugly in more subtle ways.

(I really need to take a look at this paper since it seems related to Glitch, but damned Chinese firewall)

Moderation

Moderation by censorship has lots of downsides:

1. Readers who saw the post before it was censored might want to respond to the merits / correct misunderstanding.

2. What happens to the post? Is it gone or marked [censored]? What happens to replies that made it in before moderation?

3. Once you've removed someone's comment, they're on the defensive. So you're either going to impose a temporary (thread-local?) ban or get drama posts about the moderation.

4. It requires an authority structure.

5. It's work.

If we do censor, I think we should restrict to the case you're describing: rude comments aimed at a third party work. I would prefer a follow-up post with [Moderation] as the subject line that calls out the offending behavior, possibly requesting an edit by the original poster with a citation to the rules document. I believe Anton has made similar posts. We could step this up.

Moderation

I am not too pleased with moderation either. The alternative you propose (post-facto remark requesting an edit by the original poster) would be much more lightweight and does not require a hierarchy of power/authority.

I think this could work if there was community consensus that this is a good process. One downside of course is that the original poster may not want to change the original post; but a rare author-not-willing-to-change-a-rude-post event could be an acceptable price to pay for a lightweight process (if it's indeed rare). In fact that was my previous understanding of how LtU was supposed to work *right now*, except I am not so sure after seeing how this thread went after my original remark on the form.

Sounds good to me

By the power vested in me by the Bureau of Alcohol, Tobacco and Firearms and the great state of Texas, I hereby deputize you defender of the realm and hall monitor. Make sure Anton has your mailing address and allow 30 days for your plastic badge to arrive.

(I do support your suggestion. Seconds? Objections?)

Isn't that already what

Isn't that already what happened and failed in this case?

Buy-in

Maybe what's missing is buy-in from the community. We have an LtU site policy document passed down from the Ancients, but it hasn't really been adhered to lately. Maybe start a new forum topic to request feedback on the proposed increase moderation policy? I personally think it's pretty reasonable to require politeness in the delivery of criticism of the work under discussion.

If you meant we should consider how to deal with repeated or unrepentant offenders, I suspect we could make due with a community policy to avoid responding to the rude comment until it's edited. Unless the poster is doing it frequently, a ban probably isn't warranted. If an author stops by and finds a rude comment about his paper that is followed by a request for it to be edited and all of the interesting discussion under other comments, I don't think that's a bad situation. It's the internet.

Does it go both ways?

I consider you an extremely rude person for lifting a technical remark about a paper to perceived rudeness, a remark which started with "Sorry".

I subsequently demand you personally apologize to me for ganging up on me and further demand you edit your posts.

Sorry, you have no manners whatsoever.

:)

Classic marco.

revisionism

Fwiw, I generally disapprove of editing posts; it feels too much like revising history. I'm very leery of changing my posts, and if I do for more than an obvious typo, I leave a bracketed note or the like. I've been known to apologize if I think that's warranted, but that's quite different.

I'm curious to know how you would have worded marco's post differently, to convey (I'd presume is the intention) the same technical meaning in a less objectionable way.

Maybe so

I can see that. I tossed that suggestion out with 'possibly'. I have a bad habit about using "post comment" as my preview. If I'm editing soon after posting or fixing grammar or a bad wording that doesn't change the meaning, I don't leave a note. If I'm making a substantive change after time has passed, I use brackets.

The first comment wasn't terribly rude, but the characterization of their work as "useless" and the addendum that he can't care about it were both poor choices if politeness is a goal. His second comment was an overt insult. Again, as a reader the comments didn't bother me. I don't think that style is good for the site, though.

insert title here

Well, yes. The title judges aboslute merit, which is presumptuous. The post itself judges relative merit — value for the poster — and so probably wouldn't come across badly without the provocation of the title. The final sentence of the post could be read as relative or absolute; if not for the absolute title, it'd likely be read as relative.

I am unwilling to change my post

I don't live in a meritocracy, and like the rest of the world cannot care much about that particular aspect of academia. I judge papers by usefulness to me, and I need to be convinced.

I don't know the author, neither do I care about the author. If there are good reasons I am a dork for not seeing that the paper makes a substantial contribution solving a hard problem he can explain it better than he presented it in the paper.

I didn't call the author a fraud, the remark didn't go much further than I think he solved the wrong question, possibly badly. As far as I am concerned that's not an ad-hominem or any other form of disrespect.

I fully support my post, and all the posts I ever made here on LtU.

All the posts you ever made here

That makes things simpler.

First, to Marco: unsupported categorical statements may make an argument, but they do not make a constructive argument. Just because Hewitt does it doesn't mean it's a good idea.

Second, also to Marco: it is sad to see you take this position, because you appear to be capable of constructive discussion, criticism, and engagement. It is a shame that you usually prefer to anger people instead.

Third, to everyone else: Marco is a troll. As a recent poster here, I have hesitated to speak up about this kind of thing, but as a long-time lurker, I recognize this behavior from past history. And, given a choice between a repeat of Marco's past behavior, and Marco's absence, I would prefer the latter.

Hewitt is inappropriate and annoying, but Marco is disruptive. Not only does he make long, insulting, ond unproductive posts, but he sends other posters off on long, vociferous, and unproductive threads. This is classic troll behavior, and it doesn't really matter what Marco gets out of engaging in it.

Again, it is a shame: I agree with the view that Marco could represent a valuable element of diversity. However, I value the diversity of the rest of the LtU community more, and I would rather not see a community that has a reasonable expectation of collegial conduct disrupted by people who have no intention of providing it.

Labels are not very useful,

Labels are not very useful, and they are often not very accurate.

Feelings hurt all around in this thread.

Ridiculous

I've been posting here, on and off, for ten years. I've just restarted because I have taken an interest again in a compiler I once wrote.

I've never seen or heard from you.

What about up and down

What about up and down voting? It is effective in providing anonymous immediate feedback.

dislike

This is not, and should not be, a "social media" site. We're here for serious discussion. [edit: Well... mostly serious. :p ]

A problem with up and down

A problem with up and down voting is that there's only a single bit of information in it (or actually lg(3) bits), so "incorrect, impolite, spam, dislike" all get turned into a downvote. Another thing is that they have the effect that people start to post things that tend to get upvoted, and this does not always coincide with good content. A button clearly marked as "this is inappropriate for LtU" would be a more conservative option.

Feedback can be provided as

Feedback can be provided as comments as usual. Pther down vote provides a way to easily provide feedback by lurkers who aren't interested in responding (we have many) AND is useful in curating discussions: what comments shoud I read and which ones are skip-able. We have many old discussions with good content, and up votes (of both submissions and comments) could allow new readers to more quickly hone in on that content.

Crowd sourcing is the present and the future. Moderation is so 00s.

Crowd sourcing is the

Crowd sourcing is the present and the future. Moderation is so 00s.

I think we're still learning how to do crowdsourcing, and ten years from now the ways we do it now will look very old-fashioned and naive.

I definitely hope so! The

I definitely hope so! The same with programming :)

The weak guarantees aren't

The weak guarantees aren't due to performance issues, they're due to correctness in the face of redundancy which is needed for robustness. So I disagree with your comment entirely.

Of course they are

It is stated in the introduction. Weak guarantees in exchange for scalability.

The denotational semantics look like overkill for this application. My first order approximation would be to express invariants through the type system, not derive a denotational semantics for it, and then show performance guarantees and the like.

Whatever.

They deal with guarantees for existing techniques

The problem is *reasoning about* fast abstractions for this domain. I'm not sure they're changing anything that is relevant to performance, though I can't be sure from just glancing at the contributions; but they are talking about weak consistency models, whose performance advantages have been explored to death in other contexts. (I'm not quite sure about the particular model, but they're by far not inventing eventual consistency).

What's new here is also *not* a way to reason about performance, as far as I understand. Hence, your comment about performance guarantees seems irrelevant.

What's new is a way to reason (mathematically) about correctness of programs using these abstractions. Maybe you're not interested in that problem, but others are, and we don't want to debate formal methods again. There's a difference between solving the wrong problem and solving a problem you don't care about. (Frankly, you haven't convinced us your interests are relevant to anybody, though they might well be). Denotational semantics, per se, can be appropriate for compositional reasoning.

After talking on the paper, let me talk about your contribution to the discussion.

You've IIRC stated on LtU you don't care about being polite, and *I* can somewhat live with that. You haven't studied the work in full, and I can live with that (I'm doing the same). But I'm not happy with anybody (here, you) dismissing something so rudely without having enough clue. From this distance, and from this and other comments (in earlier discussions), it seems like you're probably smart, but your arrogance borders sometimes on Dunning–Kruger, and that it prevents you from forming informed opinions. You might want to pay attention to that, and not to be nice (you don't care about 'nice', fine), but in your egoistical personal interest.

Note that I wrote "it seems like": that's not out of insincere politeness, but because I'm convinced I can't know for sure through the Internet (though I've studied other characters in person).

Shape Up.

I haven't been rude. I've dismissed the paper with an argument.

The first response was an ad-hominem.

Adults can take criticism.

I haven't been rude. I've

I haven't been rude. I've dismissed the paper with an argument.

It's interesting that you don't find "dismissal" rude. Would you "dismiss" someone's hard work right to their face, or would you instead politely point out where you think the paper may have a few weaknesses?

If LtU is to be a better community than that found on the internet in general, at least when it comes to discussions about programming languages, expecting the same courtesies we express in person seems like a promising route.

There's more room near the edge

marco could go a lot further than "the paper may have a few weaknesses" without going too far (which imho he narrowly did — but it really is a sharp drop-off, so it doesn't matter how "narrowly" you go too far, hence the hullabaloo). It's possible to stay on the sunny side of rudeness while still saying "Since the problem of replicated stores can be roughly described as: we can only provide weak guarantees due to performance issues, I can't care about this study without a performance analysis." Harsh but honest. What you don't say is "Sorry, but useless without a performance analysis". There's a vast gulf between "I can't care" (a statement about relevance to me) and "useless" (a statement about absolute lack of merit).

Like LtU should mimic Academia?

God man. I don't have time weigh all arguments precisely. There is a) the manner in which academics weigh papers among themselves, and b) the manner in which people appraise products in the rest of the world.

If I am going to buy a TV I don't worry about how much effort went into it and I am not going to tiptoe with my arguments.

This paper may be interesting amongst academics but I am thoroughly unconvinced it solves a real problem such as Facebook might have.

As stated, I cannot care about the efforts of the academic, I appreciate it on usefulness in a production environment and I don't believe it is a) that simple and b) is anything more than an over-trivialised start to something which might, but probably won't, pay off.

I either want to see complexity results or a performance analysis given an implementation.

To me, this paper squarely falls into academia's self-serving pressure to publish but IMHO from a real-world perspective probably never should have been written. Do you believe Facebook would feel helped given this paper?

I've wasted enough time on it. The original appraisal was concise, down-to-earth, and reflected my opinion.

If you cannot be polite, you can be quiet

If you find that you don't have time to express something in a respectful manner, you can also stay silent. I would prefer to have less comments to my posts than down-to-earth opinions expressed in a rude manner. In fact, having few comments is my common case, and I assume it is because the usual commenters don't care about the proposed work or didn't find the time to read it properly, and that is ok.

(Let me offer you my email, gasche dot dylc at gmail, as a place to send your down-to-earth comments if you wish to. I may not find the time to reformulate them each time, but will try to.)

Also, if the main content of a comment is "I don't care", I find it is almost always better to stay silent, no matter how graceful the idea can be expressed. The world is full of persons that do not care, and saying it out loud adds little of value. If you actually think "I don't care without more justifications of X" and are honestly interested in X, just ask "X?".

If I am going to buy a TV I don't worry about how much effort went into it and I am not going to tiptoe with my arguments.

The very point is that the appropriate form depends on the audience. If you bought, or rather if you saw in a presentation booth a hand-made TV, that was manually crafted by someone who is within earshot, you would have to formulate you argument in a different manner than with your friends in a private space.

Disagree

You post this paper therefore the paper gets comments. Moreover, instead of thinking about "does this paper need complexity results" you shifted the argument to whether I would be rude.

You haven't brought one technical argument, instead, concentrated on an ad-hominem whether I would be rude. Something I don't care about.

Moreover, you have drawn that argument into the public so I am not going to fight it out in person. You can try fight it out in public.

Weak.

misuse of 'ad hominem'

An ad-hominem is only a fallacy if it's used as a substitute for an argument against a logical point, pathos vs. logos. But I don't think anyone here is objecting to your logical point that the subject would greatly benefit from performance analysis. They're only objecting to your presentation of it.

Whether or not you care about being rude, evidently other people do care. Rather than asking "do I care whether I'm rude" (you might not, at that moment), maybe ask "do I want to spend any effort defending this rudeness?" (it's pointlessly stressful) or "do I want any risk of rudeness derailing my point?" (it happens) or "do I want LtU to become like all the other cesspits of the Internet?". Pride makes it difficult for most humans to apologize for words after they become public, even if they regret them. But it's a lot easier to temper words before or shortly after posting.

Final post and summary

Not stating a position on your tone or posting history, I will simply summarize a few points which should be evident:

* You've stated an interest in advancing your knowledge of certain topics. It's presumably why most of us are also here.

* LtU has a plethora of experts on subjects that overlap your interests, some of which are just passing through when their work is discussed. Much of LtU's value is in the technical discussion with such people.

* There are documented instances where the tone of a sub-thread has led such experts to believe that it isn't worth their time posting.

* It's been stated that some of your comments have contributed to this impression.

* If it's even remotely true, then you are actively sabotaging at least yourself. At best, experts won't reply to your questions, at worst, they won't post to LtU at all.

* Since you think adults should take honest criticism, you should consider the feedback you've been given (from multiple people no less). Unless you think the people telling you this aren't being honest?

* It's not productive to respond to a discussion about a threat to LtU's value as a whole by saying it's a non-technical response to your allegedly technical critique. A specific technical critique is irrelevant if LtU itself no longer has value.

* Even valid technical critiques look like trolling when phrased a certain way. Torvalds-style critique is only appropriate in certain contexts.

* It seems evident then, that if you want your critiques taken seriously, don't make them look like trolling. If you don't care whether your critique is taken seriously, then why take the time to post it?

* It's not hard to "politify" all of the allegedly "rude" declarative statements: just rephrase them as questions. Not being an expert on all the papers the authors have written, you presumably don't know whether a performance analysis actually exists. Asking whether it does is a perfectly polite criticism.

As an aside, this whole subthread turned into a meta-thread about LtU policy, which is now polluting the discussion of an interesting paper. It'd be nice to be able to tag/hide a subthread or move it into a new post when this happens.

Unconvincing

My small country produces 50k papers yearly. Extrapolating the US about a million yearly. Maybe, around 2.5M papers worldwide.

This paper is an academic application of operational semantics picked somewhere out of the furthest of the furthest corner of academia. It might be fine math but it isn't near anything relevant anyone with a clear mind in PLT should take an interest in.

A discussion about the l- and rvalue semantics in C++ at least would draw an audience.

As far as your arguments go, I don't care about your false pretenses.

It'd be nice to be able to

It'd be nice to be able to tag/hide a subthread or move it into a new post when this happens.

The Discourse forum platform offers a feature exactly for that, since it's been designed to foster good discussion practices (at least they say). I haven't enough insight to evaluate the Discourse claims critically, or to know how else it could help here.
Is there enough interest to open a discussion on the platform? Right now, I don't even see people complaining that LtU still requires HTML input rather than Markdown, which is the first source of technological friction with LtU for me.

solves a real problem such as Facebook might have

Ironically, the second author was a primary contributor to separation logic, the secret sauce to the spin-out company Monoidics, which was of sufficient interest to Facebook that they bought the company.

Thanks for the counterpoint

Thanks for the counterpoint

Not Ironic

Not even near ironic to be honest. I got that they try to lift verification methods to the problem of replicated data.

I just disagree with them that this is that 'easy' to follow through like they did with imperative semantics since I assume that the problem you want to solve head-on is that of performance, or algorithmic complexity.

In my opinion, if you follow along this path chances are good that you'll end up with fully verified but non-performant code trivially.

The performance demands, in my view, simply adds a new non-trivial twist to verification software demanding a much lighter approach to the verification and demanding a very heavy burden on top of what you prove correct.

This will, and should, be about performance first and correctness second.

re: performance first, correctness second

As I understand it, CRDTs are aimed at the problem of partitioning/disruption tolerance, preserving certain forms of correctness (eventual consistency, or causal consistency) under hostile network conditions.

Without compositionality, it is difficult to build rich models from CRDTs. So, the work done in the paper here has value even if the data types are slow. If I'm using CRDTs, it's because I expect unpredictable latencies anyway (ranging from fractions of a second to many days, e.g. when a mobile device goes offline with some partition of data). I wouldn't use CRDTs for the latency critical parts of an application.

Performance and correctness are both important, and are rarely in conflict. The lack of a performance analysis doesn't mean CRDTs will be slow, rather that making them fast hasn't been the priority for making them useful.

Performance paramount; Inconsistency Robustness must follow

If it is not performant, then it is irrelevant. After that, scalability and complexity make inconsistency robustness a primary issue.

How fast must an algorithm

How fast must an algorithm be to make up for the fact it gives a wrong answer? I know a very fast sorting algorithm that doesn't sort. Performant seems irrelevant without correctness.

No "correctness" for large-scale; only Inconsistency Robustness

There is no "correctness" for large-scale complex information systems.

Instead, Inconsistency Robustness becomes a goal.