4 ms·

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 l

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.

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.