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).

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.