Hi Roshan! I'm a newbie C++ programmer, but I have experience designing logic programming languages (e.g., miniKanren in Scheme). I'm curious why Castor doesn't implement full unification. Is this because of the historical relationship between Castor and Leda? There are many interesting logic programs that can't be written naturally without full unification. (My dissertation contains many such programs, so I'm biased!) Many people in the logic programming community don't consider Mercury to be a real logic programming language precisely because it doesn't support full unification. Is Castor aiming towards the Mercury model, with the idea of adding mode annotations, etc., in the future? That might be a nice sweet spot for the Boost libraries. Otherwise, I would prefer to see full unification in any official Boost logic programming language/library. How hard would it be to add full unification to Castor, or to at least allow full unification as an option? --Will