|
I used it for the first time in firmware design at MSFT a few years ago, and I've used it since in the areas of protocol design. I don't use it frequently but it's a tool I'm glad I took the time to learn, and have to hand when I need it. My experience is that, using TLA+, or other tools like it, encourages you to think precisely about the problem and at the same time exclude unnecessary details. That alone I find useful in terms of the insights it gives e.g. surfacing interesting invariants, or alternatively, invalidating them. In any case, you use the model-checker (TLC) to test these assumptions quite easily, and then bring these invariants into your code, either in the form of assertions, contracts or perhaps in property-based testing. In any case, I would say the process of writing such a specification yields benefits. Perhaps this can best be summed up by something I think Leslie Lamport once said: "If you're not writing when you're thinking, you only think you're thinking." I should add that despite claims about TLA+ being particularly well-suited to concurrency problems, my implementation targets have never been 'concurrent' in the 'multi-threaded' sense. Rather, they have been single-threaded event-driven state machines, and I personally find that it excels in this space. However, as you will find, in TLA+, concurrency is just a matter of abstraction... I have found that, because TLA+ doesn't 'generate code', many colleagues struggle to see the tangible benefit. I personally think that there is a gap between the whiteboard and the editor which tools like TLA+ fill very nicely. It's not a panacea or a magic bullet, and like any tool you must still exercise judgement about when to use it, and how to use it effectively, which includes understanding the limitations of the tooling (TLC cannot check arbitrary specifications). But if I find myself faced with a potentially tricky algorithm, or indeed want to understand an existing algorithm, I reach for TLA+. |