alt Hacker News> designing stuff with TLA+, then feeding the spec into Claude
That seems to defeat the purpose of using TLA+ in the first place. It's taking a rigorously logical and proven specification, putting it through a black box (that you don't own and cannot inspect) with indeterminate and unknown process, to get executable code that may or may not have anything to do with the specs.
Unless you feed the code back into something to verify that it corresponds with the specs? Is there nothing that can turn the specs into executable code directly and deterministically? Why involve a language model at all?
I'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.