The +CAL Algorithm Language

Leslie Lamport has extended his TLA+ Tools with +CAL, a language to specify algorithms in.  As he explains:

+CAL (pronounced "plus-CAL") is an algorithm language based on TLA+.  A +CAL algorithm is translated to a TLA+ specification, which can be checked with the TLC model checker.

An algorithm language is for writing algorithms, just as a programming language is for writing programs.  The introduction to the +CAL manual (see below) explains how algorithms differ from programs, and how +CAL differs from programming languages. 

+CAL comes with two syntaxes, one Pascal-like and the other Java-like.  This looks like a cynical attempt to attract the curly-brace rabble (but I reckon most of them would probably fail to appreciate Lamport's distinction  between an algorithm and a program).