While both TLA+ and ADA/Spark might be necessary, I haven’t noticed much mention of ADA/SPARK here, which kind of surprised me that they are not used in conjunction as frequent as I might have thought.
For some critical software we developed, we used TLA+ for high-level formal specification. As mentioned earlier, transitioning the actual implementation to another language can be challenging, especially if partial hardware bootstrapping is required. We ended up implementing the high-level specification created in TLA+ using ADA/Spark, which minimized our exposure to buffer and assertion failures. However, optimizing the code to meet performance thresholds was at times frustrating and time-consuming, like any low-level implementation with a new tool/language for us.
I’m curious about any new tools or workflows for leveraging TLA+ high-level specification implementation into other languages like C and Rust. What approaches are people taking once the formalized specification is verified in TLA+ to complete the implementation?
I might be out of the loop, but using TLA+ spec and translate then to other languages hasn’t been a successful use case for LLMs. While they can be helpful, a significant effort is still required to ensure that implementations accurately adhere to the specifications.
spaintech · · focus · HN ↗
For some critical software we developed, we used TLA+ for high-level formal specification. As mentioned earlier, transitioning the actual implementation to another language can be challenging, especially if partial hardware bootstrapping is required. We ended up implementing the high-level specification created in TLA+ using ADA/Spark, which minimized our exposure to buffer and assertion failures. However, optimizing the code to meet performance thresholds was at times frustrating and time-consuming, like any low-level implementation with a new tool/language for us.
I’m curious about any new tools or workflows for leveraging TLA+ high-level specification implementation into other languages like C and Rust. What approaches are people taking once the formalized specification is verified in TLA+ to complete the implementation?
I might be out of the loop, but using TLA+ spec and translate then to other languages hasn’t been a successful use case for LLMs. While they can be helpful, a significant effort is still required to ensure that implementations accurately adhere to the specifications.
pjmlp · · focus · HN ↗
You have to go into high integrity computing industry and related conferences to see it being used.
agentultra · · focus · HN ↗
It doesn’t fully close the specification gap but if it could be made robust it might be a good tool.
Generating code directly from the high level specification is called, synthesis, and is still in research mode.
Projects like Synquid[0] have come a ways but are still far from being able to express even trivial programs.
[0] <a href="https://www.csail.mit.edu/research/synquid-synthesis-liquid-types" rel="nofollow">https://www.csail.mit.edu/research/synquid-synthesis-liquid-...