It's more likely to be used by someone who then implements a practical tool on top of it. I used it to prove relational properties of WASM programs, which is useful to prove security properties like constant-time or differential privacy. You can also use it to prove program equivalence, which I think would be neat for testing a compiler with.