By the way, there is a similar work to Unison project. Its basic idea is to automate the compiler backend generation with help of SMT solver. The article: https://link.springer.com/epdf/10.1134/S0361768821070082?sha...