What is this algorithm computing and how to prove it?

On Hackerrank I found a test that asks to check what the following algorithm computes:

• If $x > y$ then $x = x - y$

• If $y > x$ then $y = y - x$

• If $x \neq y$ then goto 1

• Print $x$

Constraints: $x$ and $y$ are greater than $0$

So I think/guess this algorithm returns the product of common factors, so 1 when they do not have any in common. I just guessed it by computation and by intuition, but I would like to prove it in a formal way.

How can this be proved?

The algorithm computes the greatest common divisor, or gcd for short.
You are correct that the output is the product of common factors, since the gcd is known to be equivalent to it.

In fact, this algorithm is known as Euclid's algorithm.

StackExchange Computer Science Q#142678, answer score: 7