About our use case: We developed an algorithm for creating "semantic diffs" between two source code trees. Starting from a graphical (AST) representation of the source code of an entire software project, such a diff would basically tell you how you can transform one tree into the other using a range of edit operations (e.g. insert, delete, copy, paste, modify). The advantage compared to line-by-line diffs is that the latter work only on the text-level (i.e. "this line has been removed, this other line has been added"), whereas the former can actually tell you what changed on a semantic level (i.e. "this argument was inserted into this function and this variable name was changed").
For big projects, this is quite a computational challenge and can (could) only be solved using approximations and shortcuts. Having a polynomial-time algorithm for this would therefore be a huge deal.
I hope that the proof will soon lead to practical implementations of the algorithm.