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.

• Patch theories
  • Darcs
  • Inverse semigroups
• Coq
  • Type classes
  • Encoding inverse semigroups
  • Proving facts about inverse semigroups
• Conclusion

This is it! After some thoughts, I decided it was time for me to finally open a tech blog, so that my article ideas may become concrete. After a couple of days hacking to produce something I am not ashamed of showing to the public, it is now online, ready to receive some content. I really do hope I will take the time to fill it, and also hope that the content will be worth reading.

To inaugurate this blog, let’s start with a post that describes what technologies I chose to host this content.