it is totally declarative and almost like an SMT solver so has some properties that can make it more useful in certain situations - I think it might even be fully statically verifiable but not sure. would need to look it up.

I think Rust was initially using it for reference counting.