Why is the Halting problem decidable for Goto languages limited on the highest value of constants and variables?

This is taken from an old exam of my university that I am using to prepare myself for the coming exam:

Given is a language $text{Goto}_{17}^c subseteq text{Goto}$. This language contains exactly those $text{Goto}$ programs in which no constant is ever above $17$ nor any variable ever above $c$.

$Goto$ here describes the set of all programs written in the $Goto$ language made up of the following elements:

With variables $v_i in mathbb{N}$ and constants $c in mathbb{N}$
Assignment: $x_i := c, x_i := x_i pm c$
Conditional Jump: if(Comparison) goto $L_i$
Haltcommand: halt

I am currently struggling with the formalization of a proof, but this is what I have come to so far, phrased very casually:
For any given program in this set we know that it is finite. A finite program contains a finite amount of variables and a finite amount of states, or lines to be in. As such, there is a finite amount of configurations in which this process can be. If we let this program run, we can keep a list of all configurations we have seen. That is, the combination of all used variable-values and the state of the program. If we let the program run, there must be one of two things that happens eventually:
The program halts. In this case, we return YES and have decided that it halts.
The program reaches a configuration that has been recorded before. As the language is deterministic, this means that we must have gone a full loop which will exactly repeat now.

No other case can exist as that would mean that we keep running forever on finite code without repeating a configuration. This means after every step, among our list of infinite steps, there is a new configuration. This would mean that there are infinite configurations, which is a contradiction.

Is this correct? Furthermore, how would a more formal proof look if it is? If not, how would a correct proof look?