Does this have any practical uses, or is this just an attempt to push the limits of relational programming? For example, can you use this system to derive new compile-time optimizations? Or can you use it to formalize compile-time floating-point arithmetic in languages with refinement types or dependent types? The latter is a well-known pain point in Idris, for example.