[auggierose]

This seems to be a field perfect for theorem proving, I think I've seen some work by Kleppmann using Isabelle.

I once tried to understand the Yjs paper, but I came to the conclusion that their proof is just wrong! They do some impressively looking logical reasoning in the paper, but they define some order in terms of itself, so they don't really show anything, if I remember correctly. If you tried that in Isabelle, it would stop you already at the very start of all that nonsense.

[josephg]

I talked to Kevin Jahns (the author of the YATA paper & Yjs) about his paper a few years ago. He said he found errors in the algorithm described in the paper, after it was published. The algorithm he uses in Yjs is subtly different from YATA in order to fix the mistakes.

He was quite surprised the mistakes went unnoticed through the peer review process.

There have also been some (quite infamous) OT algorithm papers which contain proofs of correctness, but which later turned out to actually be incorrect. (Ie, the algorithms don't actually converge in some instances).

I'm embarassed to say I don't know Isabelle well enough to know how you would use it to prove convergence properties. But I have gotten very good at fuzz testing over the years. Its wild how many bugs in seemingly-working software I've found using the technique.

I think ideally you'd use both approaches.

[auggierose]

Ah, that makes sense! I thought that Yjs must be doing something differently than described, because it seems to work well in practice, but I couldn't see how Yata would. Anyway, I learnt a lot by thinking through that paper :-)

Fuzz testing and proof are complementary, I think, both catch things the other one might not have caught. The advantage of Fuzz testing is that it tests the real thing, not a mathematical replica of it.