News for hackers. Stuff that matters.

A comment on Learn TLA+ (2018). Parent comment

Re:Learn TLA+ (2018) by sriram_malhar on Sunday February 23, 2020 @10:37PM (#22401442)
> You're confusing TLC with TLA+.

True that. I have not really been able to get anything beyond the most trivial to work with TLC, so I just stick to TLA+.

> TLA+ is not "too abstract". It is mathematics.

I understand. I'd wager that is the chief reason why most programmers don't even begin to investigate it. Spin feels easier because it is operational and because it can incorporate C.

[ Parent | on HN ]
Re:Learn TLA+ (2018) by pron on Monday February 24, 2020 @07:59AM (#22403623)
> I have not really been able to get anything beyond the most trivial to work with TLC, so I just stick to TLA+.

Really? I personally have checked quite elaborate TLA+ specifications with TLC, and I know others have, too. Sure, like all verification tools it's got its limits, but even for a complex distributed system spec, TLC could reasonably check it with, say, four nodes.

> I'd wager that is the chief reason why most programmers don't even begin to investigate it.

I'm not sure Spin is used more than TLA+ these days, especially when it comes to "mainstream" software.

[ Parent | on HN ]