> Which is directly at odds with needing TLA+, because if you do need it, it means the complexity of the algorithms is so great, that you won't be able to keep them in your head and understand every aspect of their performance to make something work well.
Having used TLA+ for years, I would say it's the exact opposite. All bugs happen due to someone believing something is simple enough to work out in their head while it actually isn't. So if your judgment about what you can keep in your head is good, you never have any bugs and you really don't need TLA+. But if you do happen to have bugs occasionally, then your belief about how much you can keep in your head is sometimes wrong. TLA+ is a very quick way to write down what's in your head so you can think about it more rigorously. Surely, if you can truly keep it in your head, it should be easy for you to write it down precisely. And just in case you're wrong, there are tools that can check if you're right, just to be extra sure. In short, TLA+ helps if you ever have bugs. It doesn't help if you never do.
Having used TLA+ for years, I would say it's the exact opposite. All bugs happen due to someone believing something is simple enough to work out in their head while it actually isn't. So if your judgment about what you can keep in your head is good, you never have any bugs and you really don't need TLA+. But if you do happen to have bugs occasionally, then your belief about how much you can keep in your head is sometimes wrong. TLA+ is a very quick way to write down what's in your head so you can think about it more rigorously. Surely, if you can truly keep it in your head, it should be easy for you to write it down precisely. And just in case you're wrong, there are tools that can check if you're right, just to be extra sure. In short, TLA+ helps if you ever have bugs. It doesn't help if you never do.