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

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.

Applications are open for YC Summer 2018

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