3 ms·
what kinds of ways have you been applying TLA? I've been considering whether it's worth learning for practical purposes.
by Palomides 8y ago
what kinds of ways have you been applying TLA? I've been considering whether it's worth learning for practical purposes.
- agentultra 8y agoI've used it most often to understand a poorly understood piece of a system that is giving the team a lot of trouble. An example would be a feature that went into development quickly and was iteratively developed in an agile fashion. The senior developer was smart and made some diagrams and accompanying prose to describe the system from a high level. However once the system had been in production for about six months users were discovering and reporting strange behaviors. I wrote some TLA+ models to verify the design and discover the under-specified behaviors. I've also used it in the design/planning phase of a new project. We started writing models for key features and even hooked TLA+ into our CI pipeline. We planned to also integrate the TLA+ models with quickcheck so that the latter could verify our implementation based on the specification. However that didn't get too far unfortunately. TLA+ has mostly been useful in helping me understand and solve hard problems where code alone is insufficient as a specification.