Hi, thanks for the explanations!

> Having similar functionality in Ruby would be interesting. I don't know
> if it's feasible, since unification algorithms aren't particularly easy
> to write, and I don't know if it would fit with the other aspects of the
> language. The proposed unification seems like a subset of the full
> functionality of unification anyway, though, so that might be feasible.

I don't think it would be feasible.  Ruby would have to conclude
from 
X2 = Z * Z with X2 == 25
that Z == 5.  It cannot have this information, because * as a
method could mean anything.

> 
> The other proposition here is pattern matching, which is also in existing
> programming languages. Haskell has pattern matching. For example,
> lists can be built like so:
> 
> a : list
> 
> Where a is an element, list is a list, and ':' is the cons operator. However
> when writing list processing routines, you don't need to take a list and
> call head and such. What you can do is:
> 
> f (x:xs) = ...
> 

I would propose something like:
def mymethod(*[a, *b])
  [a, b]
end
mymethod [1, 2, 3, 4]
=> [1, [2, 3, 4]]

It would only be a subset of pattern matching, but interesting
on its own.

We could use := as a unify operator, it would be a combination
of comparison and assignment.
I have added these to my RCR.