[willtim]

Unison is beautiful, as it has a formal specification with proofs of correctness for its bidirectional syncing. Bi-directional syncing is hard to get right and many devs have been subsequently shown to not understand the problem fully, for example DropBox: https://www.cis.upenn.edu/~bcpierce/papers/mysteriesofdropbo...

My instinctive reaction is not to trust any brand new effort without more evidence of its correctness.

[pjc50]

> formal specification with proofs of correctness for its bidirectional syncing

Where can I find more information on this? Search is failing me.

[willtim]

There are lots of papers referenced in the "Mysteries of DropBox" paper above, but I think the full spec is here: http://www.cis.upenn.edu/~bcpierce/papers/unisonspec.pdf