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

While TLA+ itself is great, I suspect for many here that PlusCal (a "veneer" on top of TLA+) is more immediately useful. I didn't fully grasp either language until I understood PlusCal for what it is: a simple procedural language with two nondeterministic constructs, which can be used for describing concurrent state machines. Nothing more, nothing less.

(To understand PlusCal, you need first understand the basics of TLA+, but you don't need to understand the action system 100% in-depth.)

The idea behind PlusCal is to write your algorithm in it, leaving out the "unimportant" bits, and using the nondeterministic operators in place of any value that is not in your algorithm's control. The model checker, TLC, can then run all possible traces of your algorithm to search for conditions under which it may deadlock or violate some assertion you have made.

Applications are open for YC Summer 2018

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