5 ms·

Is it possible to compile algorithms from PlusCal to a traditional programming language? That way you could have a provable subcore of algorithms in your actual

Is it possible to compile algorithms from PlusCal to a traditional programming language? That way you could have a provable subcore of algorithms in your actual software project, and just autogenerate the code for the algorithms, instead of going manually from proven algorithm to hand-written implementation.

mettamage 9y ago
There is some discussion on it here about TLA+ itself: https://news.ycombinator.com/item?id=14373359 https://news.ycombinator.com/item?id=14373359 Not about JavaScript though, but C and Java.
- elcapitan 9y ago
  Thanks, will look into that - I read that Coq can generate Haskell etc, so I was wondering if something similar exists.
pron 9y ago
There is a PlusCal -> Go compiler[1] and, as I mentioned in a comment on a thread linked in another response to your question, there are tools to translate C and Java code to TLA+ for verification. But as a relatively experienced TLA+ user, I see almost no value in doing the first, and little practical value in the second. 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. That's not to say that you shouldn't also reasons about more local properties at the code level, and there are good code-level verification tools (advanced ones include Frama-C for C, OpenJML/Krakatoa for Java and SPARK for Ada) just for that. It is possible to use TLA+ (and other tools, like Coq or Isabelle) for what's known as end-to-end verification, which means verifying the important global properties all the way down to the code level (and even machine-code level), but the process is so laborious that it is virtually never worth the effort, and, in fact, it has never been achieved for any but very small programs (and even then at great cost). [1]: https://github.com/UBC-NSS/pgo https://github.com/UBC-NSS/pgo
- elcapitan 9y ago
  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.
nickpsecurity 9y ago
Although TLA+ can't, that is used extensively in some other tools like the B method, Circus for concurrency, Eshersoft's Perfect, and some provers (Isabelle/Coq). That's a good thing in my book for critical software given it knocks out errors people introduce in implementations. The only drawback is it creates simplistic code that might not be what you're wanting in performance, readability, or even security (eg side channels). Even with those drawbacks, it can become a reference implementation to equivalence check/test your hand-coded implementation against. In security, one might also mix verified/hardened implementations for untrusted input and optimized ones for trusted inputs if they come from separate, authenticated places. Lots of tradeoffs one can make with spec-to-code generation. TLA+ just isn't in that game for most languages yet. Fortunately, it's straight-forward to convert TLA+ specs to code. Thinking about how to model or fix your algorithm is where the trouble will be. ;)

mettamage 9y ago

There is some discussion on it here about TLA+ itself: https://news.ycombinator.com/item?id=14373359 https://news.ycombinator.com/item?id=14373359 Not about JavaScript though, but C and Java.

elcapitan 9y ago
Thanks, will look into that - I read that Coq can generate Haskell etc, so I was wondering if something similar exists.

pron 9y ago

There is a PlusCal -> Go compiler[1] and, as I mentioned in a comment on a thread linked in another response to your question, there are tools to translate C and Java code to TLA+ for verification. But as a relatively experienced TLA+ user, I see almost no value in doing the first, and little practical value in the second. 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. That's not to say that you shouldn't also reasons about more local properties at the code level, and there are good code-level verification tools (advanced ones include Frama-C for C, OpenJML/Krakatoa for Java and SPARK for Ada) just for that. It is possible to use TLA+ (and other tools, like Coq or Isabelle) for what's known as end-to-end verification, which means verifying the important global properties all the way down to the code level (and even machine-code level), but the process is so laborious that it is virtually never worth the effort, and, in fact, it has never been achieved for any but very small programs (and even then at great cost). [1]: https://github.com/UBC-NSS/pgo https://github.com/UBC-NSS/pgo

elcapitan 9y ago
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.

nickpsecurity 9y ago

Although TLA+ can't, that is used extensively in some other tools like the B method, Circus for concurrency, Eshersoft's Perfect, and some provers (Isabelle/Coq). That's a good thing in my book for critical software given it knocks out errors people introduce in implementations. The only drawback is it creates simplistic code that might not be what you're wanting in performance, readability, or even security (eg side channels). Even with those drawbacks, it can become a reference implementation to equivalence check/test your hand-coded implementation against. In security, one might also mix verified/hardened implementations for untrusted input and optimized ones for trusted inputs if they come from separate, authenticated places. Lots of tradeoffs one can make with spec-to-code generation. TLA+ just isn't in that game for most languages yet. Fortunately, it's straight-forward to convert TLA+ specs to code. Thinking about how to model or fix your algorithm is where the trouble will be. ;)