|
|
|
|
|
|
by virgilp
2712 days ago
|
|
|
I would still say that, though. For complex/ non-"toy" systems, the required level of detail increases so much, that if you specify it all in something like TLA+, even ignoring the performance aspects, it probably becomes too hard to understand it all and you lose most of the advantage that TLA+ is supposed to give you. It's not just about the "formal verification" part - it's about the whole cycle of model -> verify -> learn/improve understanding -> improve model. And the fact that it was used to design microprocessors doesn't say that it can or should be used to specify all the details. I bet nobody ever attempted to do the layout from the TLA+ model; it's just like in software, TLA+ was used to design geo-distributed databases... but not to write any piece of the code; just to check that the general design is right. |
|
|
Not necessarily. There are tools that compile C or Java to TLA+[1]. But, like all other code-level reasoning, when using them you are limited to very small programs.
> It's not just about the "formal verification" part - it's about the whole cycle of model -> verify -> learn/improve understanding -> improve model.
I agree, but again, that's because TLA+ is intended for industry use, not as a research tool, and as we simply don't have the technology to verify most real programs all the way down to code, TLA+ places an emphasis on the best ROI you can get from formal methods, in practice, given current technology.
[1]: https://link.springer.com/chapter/10.1007%2F978-3-319-17581-...