First, I'm not sure this is the case here, but people often confuse finite state machines with state machines (which potentially have an infinite state space).

Second, the translation from a programming language to a state-machine formalization (i.e., with an initial state set and a next-state relation) is not only relatively simple, but the result is often very succinct and clear, as those who use TLA+ can testify. It is true that very few people, comparatively speaking, use mathematical formalization of any kind, but among those who do, the state-machine formalization is the most popular by a wide margin.