> 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.
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.
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