2 ms·

I'll give a slightly different take. I work on large financial systems at $MegaCorp. Even though requirements change all the time (often because "the government

I'll give a slightly different take. I work on large financial systems at $MegaCorp. Even though requirements change all the time (often because "the government said so"), are ephemeral at best, and frequently contradictory due crossing entire teams, orgs, and charters.... Stealing every possible tool that can move the needle towards "correctness" has been crazy valuable in my experience. I've gotten on board the TLA+ train. Just the act of formally specifying what you do know makes everything you don't painfully obvious. Formal models also make dealing with that constant change easier, because The Rules live in one concrete place, in a formal modeling language, and free from the ambiguities that requirements expressed in English prose are subject to. It's not a perfect solution, but it can help cut through the noise.

pphysch 3y ago
More power to you in specifying your processes. A potential issue here is that your bosses and other stakeholders aren't part of the specification meta-process. Can you talk TLA+ with your boss? What about your boss's boss? Do they even care? A bad specification is worse than no specification; this was one of the lessons of OOP-mania (a rigid ontology works great, until it doesn't, and then it's a disaster). An ostensibly correct "specification" inferred by a lone engineer could become Wrong tomorrow after stakeholder input. That's why I would recommend against these sort of correctness-oriented paradigms unless there is widespread buy-in and understanding from your stakeholders, company culture, etc. Of course there is merit to using tools like TLA+ to model distributed systems and assist development, but that shouldn't be conflated with having a well-defined specification from the get-go.