The Learning Curve
Raw TLA+ uses mathematical notation — set theory, predicate logic, and temporal operators. It is powerful and precise, but hard for most software engineers to read and write initially. A simple specification can look like this:
Init == /\ balance = 100
/\ inFlight = {}
Next == \/ Withdraw
\/ Deposit
The /\ means logical AND, \/ means logical OR, and == means "is defined as." This is valid TLA+, but it takes time to become fluent.
Pseudocode that Compiles to Math
To lower the barrier to entry, Leslie Lamport invented PlusCal — an algorithm language that sits on top of TLA+.
PlusCal looks very similar to standard imperative pseudocode. You write loops, if-statements, and variable assignments using familiar syntax. Here is the same concept in PlusCal:
--algorithm BankTransfer
variables balance = 100;
begin
Transfer:
if balance >= amount then
balance := balance - amount;
end if;
end algorithm;
You don't run PlusCal directly. Instead, a translator (built into the TLA+ Toolbox IDE) compiles your PlusCal code into a raw TLA+ mathematical specification. This gives you the best of both worlds: you write something that looks like code, and the tools convert it into the rigorous math needed for verification.
Most engineers learning TLA+ start with PlusCal and gradually learn to read the generated TLA+ output. Over time, you gain the ability to write TLA+ directly for more complex specifications that PlusCal cannot easily express — such as specifications involving multiple simultaneously-acting processes with complex fairness conditions.