Posts tagged with “patch”
One of the open-source projects I have been working on for several years is a library that computes diffs between JSON values and produces RFC-6902 patches. Trying to go beyond what the specification proposes, I want my diff tool to generate patches that can be inverted. To this end, I just added fields to some patch operations so that missing information is remembered. I convinced myself that the fields I added are enough to invert any patch, but this is a mere conjecture. There must be a way to be sure that it works. The problem of making sure that a patch can be inverted is actually very interesting to dive into. That is how I started to investigate the area and spent the last few months to do it from time to time.
In the saga starting with this post, I want to expose how I implemented one patch theory using Coq, proved some properties on it, and applied it on an RFC-6902 implementation. There will be some theory, and, I hope, a lot of fun.
This episode defines the problem and the base theoretical tools that will be used to develop the theory.
Read more