Hacker News new | comments | show | ask | jobs | submit login

So how amenable is tla+ to automatic translation to an existing programming language?



IMO not very. It's easy in TLA+ to write things like "randomly select some bijective function from the power set of N to [0, 1]", which can be really handy for speccing but isn't exactly programming-friendly. I personally think of this as a good thing, actually. TLA+ can be simpler and more expressive than it would be if it had to also be translatable.

So you can't guarantee your implementation matches your spec. All the more reason to write unit tests!


That is not such a big problem. Many operators in TLA+ -- like division -- are defined in terms of CHOOSE, but that doesn't stop TLC from implementing them efficiently. It's very easy to supply efficient implementations for various built in constructs, and tell you that you shouldn't use CHOOSE in your own definitions that you want to be automatically translated. So the data and data operations aren't the big problem; the control state is a bigger problem: It is hard to translate TLA+ constructs to programming language idioms like subroutines, loops and threads.


You might want to investigate the Bloom project. That is the only language I know that uses temporal logic as its base while still viable for writing actual running services.

Didn't use it, but watch a few presentations, i.e: https://channel9.msdn.com/Events/Lang-NEXT/Lang-NEXT-2012/Bl...


Amenable? Probably fairly amenable. It hasn't been done yet, though. It likely wouldn't be translation so much as proving that the existing code refines a TLA+ spec.


Showing that program code refines a TLA+ spec has been done for C and Java (although scalability is a different matter).

C: http://link.springer.com/chapter/10.1007/978-3-319-17581-2_1...

Java: http://ieeexplore.ieee.org/document/6042069

The C work seems more thorough.


Amazing! I hadn't heard of this, thank you. I'll add it to the Wikipedia article.




Guidelines | FAQ | Support | API | Security | Lists | Bookmarklet | DMCA | Apply to YC | Contact

Search: