alt Hacker NewsI'm not familiar with any general purpose TLA+->regular code exporter. I think there are a few proof of concepts but as far as I'm aware nothing that has been seriously suggested for production.
I do audit the code it generates, but ultimately all I'm concerned about is the algorithm a lot of the time and since the transformation it's been generally ok. I feel like coding errors and implementation-of-the-spec errors are different things, and of course this would be an issue even if it were humans writing the code.
If you use something like Isabelle then that has direct Scala and Haskell export. I like Isabelle but personally I find that for actual engineering problems it is often too cumbersome and TLA+ is much easier to get something done.
> would be an issue even if it were humans writing
I see what you mean, that the conversion of TLA+ specs to code is error-prone in any case, regardless of who or what does the conversion.
From what I've heard, an advantage of Lean over other major theorem provers is that it can generate actual executable code (apparently C), so you get the best of both worlds: formally proven specification and the implementation. In that context, I can imagine the use of language models to assist in the generation of specs, tests, and documentation - while a (formally specified) program deterministically compiles the specs to code, or maybe interprets the specs directly to run it as code.