I'm surprised understanding the domain hasn't been mentioned. Whether I am developing for someone else or for myself, it turns out misunderstanding/misrepresenting the domain is the most common source of trouble.
If your understanding of the domain isn't thorough, is TLA+ going to be much help?
1) You have to specify your system, right? With TLA+, you can just wave you hands and say "okay this part does something, I guess." You have to force yourself to understand what, exactly, you want your system to do and what you want out of it.
2) Most systems have edge cases, side effects, and race conditions. Are you sure your design is robust against them? You might think you have good arguments for that, but wouldn't it be better to rigorously _check_?
Tests and types and stuff help you find bugs in your implementation. TLA+ helps you find bugs in your blueprints.
> “The problem is that software engineers don’t understand the problem they’re trying to solve, and don’t care to,” says Leveson, the MIT software-safety expert. The reason is that they’re too wrapped up in getting their code to work. “Software engineers like to provide all kinds of tools and stuff for coding errors,” she says, referring to IDEs. “The serious problems that have happened with software have to do with requirements, not coding errors.”
Though I think the "and don’t care to" part is a little harsh. I do care, though mostly fail. Sometimes I find it difficult to get useful information from the domain experts, and it doesn't help that domain experts often keep subtly changing the meaning of the concepts we've been working with, until nothing is left of the original and the whole system is a bit of a mess.
Yes, DDD exists to solve this very problem. It has been around since 2004 and I'm surprised to see it is still relatively unknown within the HN community.
> If your understanding of the domain isn't thorough, is TLA+ going to be much help?
I suspect it could, actually, because it lets you formalize and work with the implications of the understanding you do have without getting bogged down in the details of actual coding. Seems like this could give you the opportunity to debug your mental model much earlier in the process. (I confess I haven't actually tried TLA+, but I plan to.)
If your understanding of the domain isn't thorough, is TLA+ going to be much help?