4 ms·

Concurrent algorithms are notoriously hard. There's been tons of academic work to build models/language for concurrency, tools to check properties and so on. Y

Concurrent algorithms are notoriously hard. There's been tons of academic work to build models/language for concurrency, tools to check properties and so on. Yet, it seems nothing has emerged that practitioners actually use. I know that there are some occasional experiments (such industrial team specified their protocols using TLA+/Alloy), but it's still extremely limited. I wonder why that is.

eigenvalue 3y ago
We need automated ways of converting Python and other popular languages to TLA+ with ways of verifying that they were translated correctly. Otherwise it seems like too much work for most purposes.
- zozbot234 3y ago
  TLA+ is not intended for end-to-end verification of actually running code, that's still the domain of type systems and interactive proof checkers. You're "specifying" a toy model of how your system will behave and then verifying that.
  - eigenvalue 3y ago
    Right. But even the automatic translation/conversion from the "real" Python code (or whatever it is) to the toy model of that code would make TLA+ a lot more accessible and useful to millions of developers instead of the couple hundred at most (just a guess, maybe it's more?) that currently make serious use of it. I understand that TLA+ is not really intended for that and it's currently used more for super important, mission critical applications like flight computer code, but I would love to see that level of care and attention brought to more typical software, which even in relatively "boring" applications can involve a lot of concurrency nowadays.
    - zozbot234 3y ago
      A toy model of existing Python code is... a type system, which Python has. TLA+ is appropriate for cases where you don't even have that.
- Cieplak 3y ago
  Converting from Python to TLA+ could be considered a form of denotational semantics. It's a ton of work to model the denotational semantics of even simple computer programs. I imagine an automatic translation of a nontrivial program would be infeasible to work with, but curious if there is active research or progress in this field.
- bvrmn 3y ago
  Even small python program has enormous state beyond the reach of automatic reduction to TLA+ model. BTW TLA+ is not too hard for basic usages. I argue it's much simpler than PlusCal because doesn't have additional semantic layer.
taeric 3y ago
Modeling an entire system is almost always harder than modeling individual pieces of a system. As such, I expect that you almost always start with individual parts modeled, and then you are trying to combine multiple models together. Stated differently, no model can really account for interactions that are invisible to it. As such, unless you are aiming at a giant model that encompasses everything, it seems unlikely that you will be able to use some modeling tools that are made to do this sort of stuff directly.
Taikonerd 3y ago
I think most development occurs on problems that can't be formally modeled anyway. Most developers work on things like, "can you add this feature to the e-commerce site? And can the pop-up be blue?" which isn't really model-able. But that's not to say that formal methods are useless! We can still prove some interesting aspects of programs -- for example, that every lock that gets acquired later gets released. I think tools like Infer[0] could become common in the coming years. [0]: https://fbinfer.com/ https://fbinfer.com/
deleted 3y ago
[deleted]

eigenvalue 3y ago

We need automated ways of converting Python and other popular languages to TLA+ with ways of verifying that they were translated correctly. Otherwise it seems like too much work for most purposes.

zozbot234 3y ago
TLA+ is not intended for end-to-end verification of actually running code, that's still the domain of type systems and interactive proof checkers. You're "specifying" a toy model of how your system will behave and then verifying that.
- eigenvalue 3y ago
  Right. But even the automatic translation/conversion from the "real" Python code (or whatever it is) to the toy model of that code would make TLA+ a lot more accessible and useful to millions of developers instead of the couple hundred at most (just a guess, maybe it's more?) that currently make serious use of it. I understand that TLA+ is not really intended for that and it's currently used more for super important, mission critical applications like flight computer code, but I would love to see that level of care and attention brought to more typical software, which even in relatively "boring" applications can involve a lot of concurrency nowadays.
  - zozbot234 3y ago
    A toy model of existing Python code is... a type system, which Python has. TLA+ is appropriate for cases where you don't even have that.
Cieplak 3y ago
Converting from Python to TLA+ could be considered a form of denotational semantics. It's a ton of work to model the denotational semantics of even simple computer programs. I imagine an automatic translation of a nontrivial program would be infeasible to work with, but curious if there is active research or progress in this field.
bvrmn 3y ago
Even small python program has enormous state beyond the reach of automatic reduction to TLA+ model. BTW TLA+ is not too hard for basic usages. I argue it's much simpler than PlusCal because doesn't have additional semantic layer.

taeric 3y ago

Modeling an entire system is almost always harder than modeling individual pieces of a system. As such, I expect that you almost always start with individual parts modeled, and then you are trying to combine multiple models together. Stated differently, no model can really account for interactions that are invisible to it. As such, unless you are aiming at a giant model that encompasses everything, it seems unlikely that you will be able to use some modeling tools that are made to do this sort of stuff directly.

Taikonerd 3y ago

I think most development occurs on problems that can't be formally modeled anyway. Most developers work on things like, "can you add this feature to the e-commerce site? And can the pop-up be blue?" which isn't really model-able. But that's not to say that formal methods are useless! We can still prove some interesting aspects of programs -- for example, that every lock that gets acquired later gets released. I think tools like Infer[0] could become common in the coming years. [0]: https://fbinfer.com/ https://fbinfer.com/

deleted 3y ago

[deleted]