4 ms·

Thanks for your extensive answer! > The kind of properties you want to reason about in TLA+ are so global and fundamental, that the code you'd end up writing w

Thanks for your extensive answer! > The kind of properties you want to reason about in TLA+ are so global and fundamental, that the code you'd end up writing would both be too far removed from the high-level spec, and the process of translation would be negligible in the grand scheme of things, so that an automatic translation, if it is able to produce usable code at all, wouldn't really save you any time. Hm - the examples in the Go compiler project look relatively good though - would it make sense to use something like this for small portions of a system? I understand that modelling and transpiling an entire system is close to impossible, but a more manageable use case may be a collection of business logic algorithms that are subject to frequent change. In that case you would still want to validate each version after a change, and it would save a lot of time to just autogenerate that particular algorithm in implementation code.

pron 9y ago
Sure, it's possible to generate particular subroutines by compiling PlusCal to code, but the gains are far too small compared to the total gains of using TLA+. The kind of subroutines you'd want to model at the code-level in TLA+ would normally be very complex concurrent routines, using low-level operations that the PlusCal-to-source compiler would likely not know about (say, memory barriers), and in any case, you'd spend 98% of the time figuring out the algorithm in TLA+, anyway. Compilation would, therefore, save you 2% of your effort. As to the correctness of the generated code, we're talking very small routines here, that a careful manual translation is unlikely to get wrong. In short, the likelihood that a PlusCal compiler would know to use your chosen libraries so that you wouldn't need to modify the code anyway is low, and even if it did, the savings in both correctness and effort would be slim. A more interesting possibility would be compiling TLA+ properties into code-level specifications (such as Java's JML or C's ACSL), i.e., extracting various local properties from global ones, as that's actually "interesting" work. In general, though, you must be careful when learning about new techniques reported in research papers. In formal methods (and in many other research areas) there's a HUUUUUGE gap between what has been achieved "in the lab" and what can be made into a practical and affordable tool for industry use. TLA+ is one of a handful of formal method tools that's been put to good use in industry.
- elcapitan 9y ago
  That makes total sense. Thanks!

pron 9y ago

Sure, it's possible to generate particular subroutines by compiling PlusCal to code, but the gains are far too small compared to the total gains of using TLA+. The kind of subroutines you'd want to model at the code-level in TLA+ would normally be very complex concurrent routines, using low-level operations that the PlusCal-to-source compiler would likely not know about (say, memory barriers), and in any case, you'd spend 98% of the time figuring out the algorithm in TLA+, anyway. Compilation would, therefore, save you 2% of your effort. As to the correctness of the generated code, we're talking very small routines here, that a careful manual translation is unlikely to get wrong. In short, the likelihood that a PlusCal compiler would know to use your chosen libraries so that you wouldn't need to modify the code anyway is low, and even if it did, the savings in both correctness and effort would be slim. A more interesting possibility would be compiling TLA+ properties into code-level specifications (such as Java's JML or C's ACSL), i.e., extracting various local properties from global ones, as that's actually "interesting" work. In general, though, you must be careful when learning about new techniques reported in research papers. In formal methods (and in many other research areas) there's a HUUUUUGE gap between what has been achieved "in the lab" and what can be made into a practical and affordable tool for industry use. TLA+ is one of a handful of formal method tools that's been put to good use in industry.

elcapitan 9y ago
That makes total sense. Thanks!