There are two parts to this: writing a spec and formalizing it. Writing stuff down helps you organize, clarify and communicate your thoughts. You should write

There are two parts to this: writing a spec and formalizing it. Writing stuff down helps you organize, clarify and communicate your thoughts. You should write down a spec if you think the spec you hold in your mind can benefit from organization, clarification and communication at a level that's higher than the code. Formal means mechanical. You should write a formal spec if you feel it is complex or subtle enough to benefit from machine-aided analysis. Code is a form of formal specification (it is a specification because it describes what the system does; it is formal as it is interpretable by a computer). But code is a formal specification at a very particular level of abstraction, that may not be convenient to answer your questions. Some people think that high-level programming languages are convenient enough for the kind of analysis you want. Sometimes they are right, but often they are wrong. Explaining exactly why a language like TLA+ is more convenient than any programming language that exists or could ever exist requires some technical details (I've attempted to give a high-level explanation for why that is so here[1], but roughly, some useful levels of abstraction cannot possibly be compiled/interpreted -- as doing so in general is uncomputable -- but compilation/interpretation is a strong requirement of programming languages). However, a more concrete example of why code is insufficient is in the case of a distributed system, where you want to cocisely describe not just the behaviour of a single program, but the interaction among a set of communicating programs, the network environment and the behavior of the users (the last is relevant for any interactive system, which is a special case of a distributed one). As a rule of thumb I'd say that algorithms/systems with any non-trivial amount of concurrency (i.e. concurrent algorithms/data structures and distributed systems) can greatly benefit from a formal specification. Sequential programs may also benefit, if there is a complex interaction of rules. For example, I saw a talk that suggests formalization of the tax code as a means to find inconsistencies[2], but a business system that encodes many interacting business rules could also benefit. [1]: https://pron.github.io/posts/tlaplus_part3#algorithms-and-programs https://pron.github.io/posts/tlaplus_part3#algorithms-and-pr... [2]: https://youtu.be/EshxZVMURt4 https://youtu.be/EshxZVMURt4