Writing a formal spec in itself is a way to introduce clarity to thinking, because when writing it the spec itself lends to asking more and more questions about

Writing a formal spec in itself is a way to introduce clarity to thinking, because when writing it the spec itself lends to asking more and more questions about the things you might not have thought of. More so if there are tools to check your formal spec. But formal spec can be in higher level than the implementation. For example, it could be describing pre- and postconditions without actually stating out how to go from precondition to postcondition. I have noticed programming languages don't tend to ask the writer the right questions in the same way e.g. TLA+ and TLC do.