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?